| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . 5
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦) |
| 2 | 1 | a1i 11 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦)) |
| 3 | | iidn3 44521 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐴))) |
| 4 | | id 22 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ∀𝑥 ∈ 𝐴 Tr 𝑥) |
| 5 | | rspsbc 3879 |
. . . . . . . 8
⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥)) |
| 6 | 3, 4, 5 | ee31 44772 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥))) |
| 7 | | trsbc 44560 |
. . . . . . . 8
⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞)) |
| 8 | 7 | biimpd 229 |
. . . . . . 7
⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞)) |
| 9 | 3, 6, 8 | ee33 44541 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → Tr 𝑞))) |
| 10 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴) |
| 11 | 10 | a1i 11 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)) |
| 12 | | elintg 4954 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∩ 𝐴
→ (𝑦 ∈ ∩ 𝐴
↔ ∀𝑞 ∈
𝐴 𝑦 ∈ 𝑞)) |
| 13 | 12 | ibi 267 |
. . . . . . . 8
⊢ (𝑦 ∈ ∩ 𝐴
→ ∀𝑞 ∈
𝐴 𝑦 ∈ 𝑞) |
| 14 | 11, 13 | syl6 35 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞)) |
| 15 | | rsp 3247 |
. . . . . . 7
⊢
(∀𝑞 ∈
𝐴 𝑦 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)) |
| 16 | 14, 15 | syl6 35 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞))) |
| 17 | | trel 5268 |
. . . . . . 7
⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞)) |
| 18 | 17 | expd 415 |
. . . . . 6
⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞))) |
| 19 | 9, 2, 16, 18 | ee323 44528 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞))) |
| 20 | 19 | ralrimdv 3152 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞)) |
| 21 | | elintg 4954 |
. . . . 5
⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞)) |
| 22 | 21 | biimprd 248 |
. . . 4
⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴)) |
| 23 | 2, 20, 22 | syl6c 70 |
. . 3
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)) |
| 24 | 23 | alrimivv 1928 |
. 2
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)) |
| 25 | | dftr2 5261 |
. 2
⊢ (Tr ∩ 𝐴
↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)) |
| 26 | 24, 25 | sylibr 234 |
1
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → Tr ∩ 𝐴) |