Step | Hyp | Ref
| Expression |
1 | | dftr3 4756 |
. . . . 5
⊢ (Tr 𝑥 ↔ ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥) |
2 | 1 | ralbii 2980 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥) |
3 | | df-ral 2917 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝑦 ⊆ 𝑥 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
4 | 3 | ralbii 2980 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
5 | | ralcom4 3224 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
6 | 4, 5 | bitri 264 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥 ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
7 | 2, 6 | sylbb 209 |
. . 3
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
8 | | ralim 2948 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥) → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
9 | 7, 8 | sylg 1750 |
. 2
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
10 | | dftr3 4756 |
. . 3
⊢ (Tr ∩ 𝐴
↔ ∀𝑦 ∈
∩ 𝐴𝑦 ⊆ ∩ 𝐴) |
11 | | df-ral 2917 |
. . . 4
⊢
(∀𝑦 ∈
∩ 𝐴𝑦 ⊆ ∩ 𝐴 ↔ ∀𝑦(𝑦 ∈ ∩ 𝐴 → 𝑦 ⊆ ∩ 𝐴)) |
12 | | vex 3203 |
. . . . . . 7
⊢ 𝑦 ∈ V |
13 | 12 | elint2 4482 |
. . . . . 6
⊢ (𝑦 ∈ ∩ 𝐴
↔ ∀𝑥 ∈
𝐴 𝑦 ∈ 𝑥) |
14 | | ssint 4493 |
. . . . . 6
⊢ (𝑦 ⊆ ∩ 𝐴
↔ ∀𝑥 ∈
𝐴 𝑦 ⊆ 𝑥) |
15 | 13, 14 | imbi12i 340 |
. . . . 5
⊢ ((𝑦 ∈ ∩ 𝐴
→ 𝑦 ⊆ ∩ 𝐴)
↔ (∀𝑥 ∈
𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
16 | 15 | albii 1747 |
. . . 4
⊢
(∀𝑦(𝑦 ∈ ∩ 𝐴
→ 𝑦 ⊆ ∩ 𝐴)
↔ ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
17 | 11, 16 | bitri 264 |
. . 3
⊢
(∀𝑦 ∈
∩ 𝐴𝑦 ⊆ ∩ 𝐴 ↔ ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
18 | 10, 17 | bitri 264 |
. 2
⊢ (Tr ∩ 𝐴
↔ ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
19 | 9, 18 | sylibr 224 |
1
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → Tr ∩ 𝐴) |