Step | Hyp | Ref
| Expression |
1 | | idn2 37859 |
. . . . . . . 8
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ) |
2 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴) |
3 | 1, 2 | e2 37877 |
. . . . . . 7
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ 𝑦 ∈ ∪ 𝐴 ) |
4 | | eluni 4375 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)) |
5 | 4 | biimpi 205 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝐴
→ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)) |
6 | 3, 5 | e2 37877 |
. . . . . 6
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ) |
7 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦) |
8 | 1, 7 | e2 37877 |
. . . . . . . . . . 11
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
9 | | idn3 37861 |
. . . . . . . . . . . 12
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ) |
10 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞) |
11 | 9, 10 | e3 37985 |
. . . . . . . . . . 11
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑦 ∈ 𝑞 ) |
12 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴) |
13 | 9, 12 | e3 37985 |
. . . . . . . . . . . 12
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑞 ∈ 𝐴 ) |
14 | | idn1 37811 |
. . . . . . . . . . . . 13
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ ∀𝑥 ∈ 𝐴 Tr 𝑥 ) |
15 | | rspsbc 3484 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥)) |
16 | 15 | com12 32 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥)) |
17 | 14, 13, 16 | e13 37996 |
. . . . . . . . . . . 12
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ [𝑞 / 𝑥]Tr 𝑥 ) |
18 | | trsbc 37771 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞)) |
19 | 18 | biimpd 218 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞)) |
20 | 13, 17, 19 | e33 37982 |
. . . . . . . . . . 11
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ Tr 𝑞 ) |
21 | | trel 4687 |
. . . . . . . . . . . 12
⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞)) |
22 | 21 | expdcom 454 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → (Tr 𝑞 → 𝑧 ∈ 𝑞))) |
23 | 8, 11, 20, 22 | e233 38013 |
. . . . . . . . . 10
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑧 ∈ 𝑞 ) |
24 | | elunii 4377 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) |
25 | 24 | ex 449 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴)) |
26 | 23, 13, 25 | e33 37982 |
. . . . . . . . 9
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) , (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) ▶ 𝑧 ∈ ∪ 𝐴 ) |
27 | 26 | in3 37855 |
. . . . . . . 8
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
28 | 27 | gen21 37865 |
. . . . . . 7
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ ∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
29 | | 19.23v 1889 |
. . . . . . . 8
⊢
(∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ↔ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
30 | 29 | biimpi 205 |
. . . . . . 7
⊢
(∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
31 | 28, 30 | e2 37877 |
. . . . . 6
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
32 | | pm2.27 41 |
. . . . . 6
⊢
(∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → ((∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
33 | 6, 31, 32 | e22 37917 |
. . . . 5
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) ▶ 𝑧 ∈ ∪ 𝐴 ) |
34 | 33 | in2 37851 |
. . . 4
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
35 | 34 | gen12 37864 |
. . 3
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) ) |
36 | | dftr2 4682 |
. . . 4
⊢ (Tr ∪ 𝐴
↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)) |
37 | 36 | biimpri 217 |
. . 3
⊢
(∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) → Tr ∪ 𝐴) |
38 | 35, 37 | e1a 37873 |
. 2
⊢ ( ∀𝑥 ∈ 𝐴 Tr 𝑥 ▶ Tr ∪ 𝐴 ) |
39 | 38 | in1 37808 |
1
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → Tr ∪ 𝐴) |