Proof of Theorem orduninsuc
Step | Hyp | Ref
| Expression |
1 | | ordeleqon 7566 |
. 2
⊢ (Ord
𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) |
2 | | id 22 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ On, 𝐴, ∅) → 𝐴 = if(𝐴 ∈ On, 𝐴, ∅)) |
3 | | unieq 4830 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ On, 𝐴, ∅) → ∪ 𝐴 =
∪ if(𝐴 ∈ On, 𝐴, ∅)) |
4 | 2, 3 | eqeq12d 2753 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ On, 𝐴, ∅) → (𝐴 = ∪ 𝐴 ↔ if(𝐴 ∈ On, 𝐴, ∅) = ∪
if(𝐴 ∈ On, 𝐴, ∅))) |
5 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ On, 𝐴, ∅) → (𝐴 = suc 𝑥 ↔ if(𝐴 ∈ On, 𝐴, ∅) = suc 𝑥)) |
6 | 5 | rexbidv 3216 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ On, 𝐴, ∅) → (∃𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ∃𝑥 ∈ On if(𝐴 ∈ On, 𝐴, ∅) = suc 𝑥)) |
7 | 6 | notbid 321 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ On, 𝐴, ∅) → (¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ¬ ∃𝑥 ∈ On if(𝐴 ∈ On, 𝐴, ∅) = suc 𝑥)) |
8 | 4, 7 | bibi12d 349 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ On, 𝐴, ∅) → ((𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (if(𝐴 ∈ On, 𝐴, ∅) = ∪
if(𝐴 ∈ On, 𝐴, ∅) ↔ ¬
∃𝑥 ∈ On if(𝐴 ∈ On, 𝐴, ∅) = suc 𝑥))) |
9 | | 0elon 6266 |
. . . . . 6
⊢ ∅
∈ On |
10 | 9 | elimel 4508 |
. . . . 5
⊢ if(𝐴 ∈ On, 𝐴, ∅) ∈ On |
11 | 10 | onuninsuci 7619 |
. . . 4
⊢ (if(𝐴 ∈ On, 𝐴, ∅) = ∪
if(𝐴 ∈ On, 𝐴, ∅) ↔ ¬
∃𝑥 ∈ On if(𝐴 ∈ On, 𝐴, ∅) = suc 𝑥) |
12 | 8, 11 | dedth 4497 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 = ∪
𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
13 | | unon 7610 |
. . . . . 6
⊢ ∪ On = On |
14 | 13 | eqcomi 2746 |
. . . . 5
⊢ On =
∪ On |
15 | | onprc 7562 |
. . . . . . . 8
⊢ ¬ On
∈ V |
16 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
17 | 16 | sucex 7590 |
. . . . . . . . 9
⊢ suc 𝑥 ∈ V |
18 | | eleq1 2825 |
. . . . . . . . 9
⊢ (On = suc
𝑥 → (On ∈ V
↔ suc 𝑥 ∈
V)) |
19 | 17, 18 | mpbiri 261 |
. . . . . . . 8
⊢ (On = suc
𝑥 → On ∈
V) |
20 | 15, 19 | mto 200 |
. . . . . . 7
⊢ ¬ On
= suc 𝑥 |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ On → ¬ On = suc
𝑥) |
22 | 21 | nrex 3188 |
. . . . 5
⊢ ¬
∃𝑥 ∈ On On = suc
𝑥 |
23 | 14, 22 | 2th 267 |
. . . 4
⊢ (On =
∪ On ↔ ¬ ∃𝑥 ∈ On On = suc 𝑥) |
24 | | id 22 |
. . . . . 6
⊢ (𝐴 = On → 𝐴 = On) |
25 | | unieq 4830 |
. . . . . 6
⊢ (𝐴 = On → ∪ 𝐴 =
∪ On) |
26 | 24, 25 | eqeq12d 2753 |
. . . . 5
⊢ (𝐴 = On → (𝐴 = ∪ 𝐴 ↔ On = ∪ On)) |
27 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝐴 = On → (𝐴 = suc 𝑥 ↔ On = suc 𝑥)) |
28 | 27 | rexbidv 3216 |
. . . . . 6
⊢ (𝐴 = On → (∃𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ∃𝑥 ∈ On On = suc 𝑥)) |
29 | 28 | notbid 321 |
. . . . 5
⊢ (𝐴 = On → (¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ¬ ∃𝑥 ∈ On On = suc 𝑥)) |
30 | 26, 29 | bibi12d 349 |
. . . 4
⊢ (𝐴 = On → ((𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (On = ∪
On ↔ ¬ ∃𝑥
∈ On On = suc 𝑥))) |
31 | 23, 30 | mpbiri 261 |
. . 3
⊢ (𝐴 = On → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
32 | 12, 31 | jaoi 857 |
. 2
⊢ ((𝐴 ∈ On ∨ 𝐴 = On) → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
33 | 1, 32 | sylbi 220 |
1
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |