Step | Hyp | Ref
| Expression |
1 | | dftr3 4105 |
. . . . . 6
⊢ (Tr 𝑥 ↔ ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥) |
2 | 1 | ralbii 2483 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥) |
3 | 2 | biimpi 120 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥) |
4 | | df-ral 2460 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 𝑦 ⊆ 𝑥 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
5 | 4 | ralbii 2483 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
6 | | ralcom4 2759 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
7 | 5, 6 | bitri 184 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥 ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
8 | 3, 7 | sylib 122 |
. . 3
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
9 | | ralim 2536 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥) → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
10 | 9 | alimi 1455 |
. . 3
⊢
(∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥) → ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
11 | 8, 10 | syl 14 |
. 2
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
12 | | dftr3 4105 |
. . 3
⊢ (Tr ∩ 𝐴
↔ ∀𝑦 ∈
∩ 𝐴𝑦 ⊆ ∩ 𝐴) |
13 | | df-ral 2460 |
. . . 4
⊢
(∀𝑦 ∈
∩ 𝐴𝑦 ⊆ ∩ 𝐴 ↔ ∀𝑦(𝑦 ∈ ∩ 𝐴 → 𝑦 ⊆ ∩ 𝐴)) |
14 | | vex 2740 |
. . . . . . 7
⊢ 𝑦 ∈ V |
15 | 14 | elint2 3851 |
. . . . . 6
⊢ (𝑦 ∈ ∩ 𝐴
↔ ∀𝑥 ∈
𝐴 𝑦 ∈ 𝑥) |
16 | | ssint 3860 |
. . . . . 6
⊢ (𝑦 ⊆ ∩ 𝐴
↔ ∀𝑥 ∈
𝐴 𝑦 ⊆ 𝑥) |
17 | 15, 16 | imbi12i 239 |
. . . . 5
⊢ ((𝑦 ∈ ∩ 𝐴
→ 𝑦 ⊆ ∩ 𝐴)
↔ (∀𝑥 ∈
𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
18 | 17 | albii 1470 |
. . . 4
⊢
(∀𝑦(𝑦 ∈ ∩ 𝐴
→ 𝑦 ⊆ ∩ 𝐴)
↔ ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
19 | 13, 18 | bitri 184 |
. . 3
⊢
(∀𝑦 ∈
∩ 𝐴𝑦 ⊆ ∩ 𝐴 ↔ ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
20 | 12, 19 | bitri 184 |
. 2
⊢ (Tr ∩ 𝐴
↔ ∀𝑦(∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
21 | 11, 20 | sylibr 134 |
1
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → Tr ∩ 𝐴) |