Proof of Theorem onuninsuci
Step | Hyp | Ref
| Expression |
1 | | onssi.1 |
. . . . . . 7
⊢ 𝐴 ∈ On |
2 | 1 | onirri 6373 |
. . . . . 6
⊢ ¬
𝐴 ∈ 𝐴 |
3 | | id 22 |
. . . . . . . 8
⊢ (𝐴 = ∪
𝐴 → 𝐴 = ∪ 𝐴) |
4 | | df-suc 6272 |
. . . . . . . . . . . 12
⊢ suc 𝑥 = (𝑥 ∪ {𝑥}) |
5 | 4 | eqeq2i 2751 |
. . . . . . . . . . 11
⊢ (𝐴 = suc 𝑥 ↔ 𝐴 = (𝑥 ∪ {𝑥})) |
6 | | unieq 4850 |
. . . . . . . . . . 11
⊢ (𝐴 = (𝑥 ∪ {𝑥}) → ∪ 𝐴 = ∪
(𝑥 ∪ {𝑥})) |
7 | 5, 6 | sylbi 216 |
. . . . . . . . . 10
⊢ (𝐴 = suc 𝑥 → ∪ 𝐴 = ∪
(𝑥 ∪ {𝑥})) |
8 | | uniun 4864 |
. . . . . . . . . . 11
⊢ ∪ (𝑥
∪ {𝑥}) = (∪ 𝑥
∪ ∪ {𝑥}) |
9 | | vex 3436 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
10 | 9 | unisn 4861 |
. . . . . . . . . . . 12
⊢ ∪ {𝑥}
= 𝑥 |
11 | 10 | uneq2i 4094 |
. . . . . . . . . . 11
⊢ (∪ 𝑥
∪ ∪ {𝑥}) = (∪ 𝑥 ∪ 𝑥) |
12 | 8, 11 | eqtri 2766 |
. . . . . . . . . 10
⊢ ∪ (𝑥
∪ {𝑥}) = (∪ 𝑥
∪ 𝑥) |
13 | 7, 12 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝐴 = suc 𝑥 → ∪ 𝐴 = (∪
𝑥 ∪ 𝑥)) |
14 | | tron 6289 |
. . . . . . . . . . . 12
⊢ Tr
On |
15 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝐴 = suc 𝑥 → (𝐴 ∈ On ↔ suc 𝑥 ∈ On)) |
16 | 1, 15 | mpbii 232 |
. . . . . . . . . . . 12
⊢ (𝐴 = suc 𝑥 → suc 𝑥 ∈ On) |
17 | | trsuc 6350 |
. . . . . . . . . . . 12
⊢ ((Tr On
∧ suc 𝑥 ∈ On)
→ 𝑥 ∈
On) |
18 | 14, 16, 17 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝐴 = suc 𝑥 → 𝑥 ∈ On) |
19 | | eloni 6276 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → Ord 𝑥) |
20 | | ordtr 6280 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑥 → Tr 𝑥) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → Tr 𝑥) |
22 | | df-tr 5192 |
. . . . . . . . . . . 12
⊢ (Tr 𝑥 ↔ ∪ 𝑥
⊆ 𝑥) |
23 | 21, 22 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → ∪ 𝑥
⊆ 𝑥) |
24 | 18, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 = suc 𝑥 → ∪ 𝑥 ⊆ 𝑥) |
25 | | ssequn1 4114 |
. . . . . . . . . 10
⊢ (∪ 𝑥
⊆ 𝑥 ↔ (∪ 𝑥
∪ 𝑥) = 𝑥) |
26 | 24, 25 | sylib 217 |
. . . . . . . . 9
⊢ (𝐴 = suc 𝑥 → (∪ 𝑥 ∪ 𝑥) = 𝑥) |
27 | 13, 26 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝐴 = suc 𝑥 → ∪ 𝐴 = 𝑥) |
28 | 3, 27 | sylan9eqr 2800 |
. . . . . . 7
⊢ ((𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) → 𝐴 = 𝑥) |
29 | 9 | sucid 6345 |
. . . . . . . . 9
⊢ 𝑥 ∈ suc 𝑥 |
30 | | eleq2 2827 |
. . . . . . . . 9
⊢ (𝐴 = suc 𝑥 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ suc 𝑥)) |
31 | 29, 30 | mpbiri 257 |
. . . . . . . 8
⊢ (𝐴 = suc 𝑥 → 𝑥 ∈ 𝐴) |
32 | 31 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) → 𝑥 ∈ 𝐴) |
33 | 28, 32 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) → 𝐴 ∈ 𝐴) |
34 | 2, 33 | mto 196 |
. . . . 5
⊢ ¬
(𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) |
35 | 34 | imnani 401 |
. . . 4
⊢ (𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴) |
36 | 35 | rexlimivw 3211 |
. . 3
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴) |
37 | | onuni 7638 |
. . . . 5
⊢ (𝐴 ∈ On → ∪ 𝐴
∈ On) |
38 | 1, 37 | ax-mp 5 |
. . . 4
⊢ ∪ 𝐴
∈ On |
39 | 1 | onuniorsuci 7686 |
. . . . 5
⊢ (𝐴 = ∪
𝐴 ∨ 𝐴 = suc ∪ 𝐴) |
40 | 39 | ori 858 |
. . . 4
⊢ (¬
𝐴 = ∪ 𝐴
→ 𝐴 = suc ∪ 𝐴) |
41 | | suceq 6331 |
. . . . 5
⊢ (𝑥 = ∪
𝐴 → suc 𝑥 = suc ∪ 𝐴) |
42 | 41 | rspceeqv 3575 |
. . . 4
⊢ ((∪ 𝐴
∈ On ∧ 𝐴 = suc
∪ 𝐴) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
43 | 38, 40, 42 | sylancr 587 |
. . 3
⊢ (¬
𝐴 = ∪ 𝐴
→ ∃𝑥 ∈ On
𝐴 = suc 𝑥) |
44 | 36, 43 | impbii 208 |
. 2
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 ↔ ¬ 𝐴 = ∪ 𝐴) |
45 | 44 | con2bii 358 |
1
⊢ (𝐴 = ∪
𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥) |