Proof of Theorem onuninsuci
Step | Hyp | Ref
| Expression |
1 | | onssi.1 |
. . . . . . 7
⊢ 𝐴 ∈ On |
2 | 1 | onirri 5751 |
. . . . . 6
⊢ ¬
𝐴 ∈ 𝐴 |
3 | | id 22 |
. . . . . . . 8
⊢ (𝐴 = ∪
𝐴 → 𝐴 = ∪ 𝐴) |
4 | | df-suc 5646 |
. . . . . . . . . . . 12
⊢ suc 𝑥 = (𝑥 ∪ {𝑥}) |
5 | 4 | eqeq2i 2622 |
. . . . . . . . . . 11
⊢ (𝐴 = suc 𝑥 ↔ 𝐴 = (𝑥 ∪ {𝑥})) |
6 | | unieq 4380 |
. . . . . . . . . . 11
⊢ (𝐴 = (𝑥 ∪ {𝑥}) → ∪ 𝐴 = ∪
(𝑥 ∪ {𝑥})) |
7 | 5, 6 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐴 = suc 𝑥 → ∪ 𝐴 = ∪
(𝑥 ∪ {𝑥})) |
8 | | uniun 4392 |
. . . . . . . . . . 11
⊢ ∪ (𝑥
∪ {𝑥}) = (∪ 𝑥
∪ ∪ {𝑥}) |
9 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
10 | 9 | unisn 4387 |
. . . . . . . . . . . 12
⊢ ∪ {𝑥}
= 𝑥 |
11 | 10 | uneq2i 3726 |
. . . . . . . . . . 11
⊢ (∪ 𝑥
∪ ∪ {𝑥}) = (∪ 𝑥 ∪ 𝑥) |
12 | 8, 11 | eqtri 2632 |
. . . . . . . . . 10
⊢ ∪ (𝑥
∪ {𝑥}) = (∪ 𝑥
∪ 𝑥) |
13 | 7, 12 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝐴 = suc 𝑥 → ∪ 𝐴 = (∪
𝑥 ∪ 𝑥)) |
14 | | tron 5663 |
. . . . . . . . . . . 12
⊢ Tr
On |
15 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝐴 = suc 𝑥 → (𝐴 ∈ On ↔ suc 𝑥 ∈ On)) |
16 | 1, 15 | mpbii 222 |
. . . . . . . . . . . 12
⊢ (𝐴 = suc 𝑥 → suc 𝑥 ∈ On) |
17 | | trsuc 5727 |
. . . . . . . . . . . 12
⊢ ((Tr On
∧ suc 𝑥 ∈ On)
→ 𝑥 ∈
On) |
18 | 14, 16, 17 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝐴 = suc 𝑥 → 𝑥 ∈ On) |
19 | | eloni 5650 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → Ord 𝑥) |
20 | | ordtr 5654 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑥 → Tr 𝑥) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → Tr 𝑥) |
22 | | df-tr 4681 |
. . . . . . . . . . . 12
⊢ (Tr 𝑥 ↔ ∪ 𝑥
⊆ 𝑥) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → ∪ 𝑥
⊆ 𝑥) |
24 | 18, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 = suc 𝑥 → ∪ 𝑥 ⊆ 𝑥) |
25 | | ssequn1 3745 |
. . . . . . . . . 10
⊢ (∪ 𝑥
⊆ 𝑥 ↔ (∪ 𝑥
∪ 𝑥) = 𝑥) |
26 | 24, 25 | sylib 207 |
. . . . . . . . 9
⊢ (𝐴 = suc 𝑥 → (∪ 𝑥 ∪ 𝑥) = 𝑥) |
27 | 13, 26 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝐴 = suc 𝑥 → ∪ 𝐴 = 𝑥) |
28 | 3, 27 | sylan9eqr 2666 |
. . . . . . 7
⊢ ((𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) → 𝐴 = 𝑥) |
29 | 9 | sucid 5721 |
. . . . . . . . 9
⊢ 𝑥 ∈ suc 𝑥 |
30 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝐴 = suc 𝑥 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ suc 𝑥)) |
31 | 29, 30 | mpbiri 247 |
. . . . . . . 8
⊢ (𝐴 = suc 𝑥 → 𝑥 ∈ 𝐴) |
32 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) → 𝑥 ∈ 𝐴) |
33 | 28, 32 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) → 𝐴 ∈ 𝐴) |
34 | 2, 33 | mto 187 |
. . . . 5
⊢ ¬
(𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴) |
35 | 34 | imnani 438 |
. . . 4
⊢ (𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴) |
36 | 35 | rexlimivw 3011 |
. . 3
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴) |
37 | | onuni 6885 |
. . . . 5
⊢ (𝐴 ∈ On → ∪ 𝐴
∈ On) |
38 | 1, 37 | ax-mp 5 |
. . . 4
⊢ ∪ 𝐴
∈ On |
39 | 1 | onuniorsuci 6931 |
. . . . 5
⊢ (𝐴 = ∪
𝐴 ∨ 𝐴 = suc ∪ 𝐴) |
40 | 39 | ori 389 |
. . . 4
⊢ (¬
𝐴 = ∪ 𝐴
→ 𝐴 = suc ∪ 𝐴) |
41 | | suceq 5707 |
. . . . . 6
⊢ (𝑥 = ∪
𝐴 → suc 𝑥 = suc ∪ 𝐴) |
42 | 41 | eqeq2d 2620 |
. . . . 5
⊢ (𝑥 = ∪
𝐴 → (𝐴 = suc 𝑥 ↔ 𝐴 = suc ∪ 𝐴)) |
43 | 42 | rspcev 3282 |
. . . 4
⊢ ((∪ 𝐴
∈ On ∧ 𝐴 = suc
∪ 𝐴) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
44 | 38, 40, 43 | sylancr 694 |
. . 3
⊢ (¬
𝐴 = ∪ 𝐴
→ ∃𝑥 ∈ On
𝐴 = suc 𝑥) |
45 | 36, 44 | impbii 198 |
. 2
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 ↔ ¬ 𝐴 = ∪ 𝐴) |
46 | 45 | con2bii 346 |
1
⊢ (𝐴 = ∪
𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥) |