| Step | Hyp | Ref
| Expression |
| 1 | | idn2 44633 |
. . . . . . . 8
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ) |
| 2 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴) |
| 3 | 1, 2 | e2 44651 |
. . . . . . 7
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ 𝑦 ∈ ∪ 𝐴 ) |
| 4 | | eluni 4910 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)) |
| 5 | 4 | biimpi 216 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝐴
→ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)) |
| 6 | 3, 5 | e2 44651 |
. . . . . 6
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ) |
| 7 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦) |
| 8 | 1, 7 | e2 44651 |
. . . . . . . . . . 11
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
| 9 | | idn3 44635 |
. . . . . . . . . . . 12
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ) |
| 10 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞) |
| 11 | 9, 10 | e3 44757 |
. . . . . . . . . . 11
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑦 ∈ 𝑞 ) |
| 12 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴) |
| 13 | 9, 12 | e3 44757 |
. . . . . . . . . . . 12
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑞 ∈ 𝐴 ) |
| 14 | | idn1 44594 |
. . . . . . . . . . . . 13
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ ∀𝑥 ∈ 𝐴 Tr 𝑥 ) |
| 15 | | rspsbc 3879 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥)) |
| 16 | 15 | com12 32 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥)) |
| 17 | 14, 13, 16 | e13 44768 |
. . . . . . . . . . . 12
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ [𝑞 / 𝑥]Tr 𝑥 ) |
| 18 | | trsbc 44560 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞)) |
| 19 | 18 | biimpd 229 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞)) |
| 20 | 13, 17, 19 | e33 44754 |
. . . . . . . . . . 11
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ Tr 𝑞 ) |
| 21 | | trel 5268 |
. . . . . . . . . . . 12
⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞)) |
| 22 | 21 | expdcom 414 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → (Tr 𝑞 → 𝑧 ∈ 𝑞))) |
| 23 | 8, 11, 20, 22 | e233 44785 |
. . . . . . . . . 10
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑧 ∈ 𝑞 ) |
| 24 | | elunii 4912 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) |
| 25 | 24 | ex 412 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴)) |
| 26 | 23, 13, 25 | e33 44754 |
. . . . . . . . 9
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑧 ∈ ∪ 𝐴 ) |
| 27 | 26 | in3 44629 |
. . . . . . . 8
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
| 28 | 27 | gen21 44639 |
. . . . . . 7
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ ∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
| 29 | | 19.23v 1942 |
. . . . . . . 8
⊢
(∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ↔ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
| 30 | 29 | biimpi 216 |
. . . . . . 7
⊢
(∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
| 31 | 28, 30 | e2 44651 |
. . . . . 6
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
| 32 | | pm2.27 42 |
. . . . . 6
⊢
(∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → ((∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
| 33 | 6, 31, 32 | e22 44691 |
. . . . 5
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ 𝑧 ∈ ∪ 𝐴 ) |
| 34 | 33 | in2 44625 |
. . . 4
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
| 35 | 34 | gen12 44638 |
. . 3
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
| 36 | | dftr2 5261 |
. . . 4
⊢ (Tr ∪ 𝐴
↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
| 37 | 36 | biimpri 228 |
. . 3
⊢
(∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) → Tr ∪ 𝐴) |
| 38 | 35, 37 | e1a 44647 |
. 2
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ Tr ∪ 𝐴 ) |
| 39 | 38 | in1 44591 |
1
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → Tr ∪ 𝐴) |