| Step | Hyp | Ref
| Expression |
| 1 | | 1n0 8526 |
. . . . . . 7
⊢
1o ≠ ∅ |
| 2 | | neeq1 3003 |
. . . . . . 7
⊢
((rank‘𝐴) =
1o → ((rank‘𝐴) ≠ ∅ ↔ 1o ≠
∅)) |
| 3 | 1, 2 | mpbiri 258 |
. . . . . 6
⊢
((rank‘𝐴) =
1o → (rank‘𝐴) ≠ ∅) |
| 4 | 3 | neneqd 2945 |
. . . . 5
⊢
((rank‘𝐴) =
1o → ¬ (rank‘𝐴) = ∅) |
| 5 | | fvprc 6898 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
(rank‘𝐴) =
∅) |
| 6 | 4, 5 | nsyl2 141 |
. . . 4
⊢
((rank‘𝐴) =
1o → 𝐴
∈ V) |
| 7 | | fveqeq2 6915 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((rank‘𝑥) = 1o ↔ (rank‘𝐴) =
1o)) |
| 8 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 = 1o ↔ 𝐴 = 1o)) |
| 9 | 7, 8 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((rank‘𝑥) = 1o → 𝑥 = 1o) ↔ ((rank‘𝐴) = 1o → 𝐴 =
1o))) |
| 10 | | neeq1 3003 |
. . . . . . . 8
⊢
((rank‘𝑥) =
1o → ((rank‘𝑥) ≠ ∅ ↔ 1o ≠
∅)) |
| 11 | 1, 10 | mpbiri 258 |
. . . . . . 7
⊢
((rank‘𝑥) =
1o → (rank‘𝑥) ≠ ∅) |
| 12 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 13 | 12 | rankeq0 9901 |
. . . . . . . 8
⊢ (𝑥 = ∅ ↔
(rank‘𝑥) =
∅) |
| 14 | 13 | necon3bii 2993 |
. . . . . . 7
⊢ (𝑥 ≠ ∅ ↔
(rank‘𝑥) ≠
∅) |
| 15 | 11, 14 | sylibr 234 |
. . . . . 6
⊢
((rank‘𝑥) =
1o → 𝑥 ≠
∅) |
| 16 | 12 | rankval 9856 |
. . . . . . . 8
⊢
(rank‘𝑥) =
∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} |
| 17 | 16 | eqeq1i 2742 |
. . . . . . 7
⊢
((rank‘𝑥) =
1o ↔ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} =
1o) |
| 18 | | ssrab2 4080 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ⊆ On |
| 19 | | elirr 9637 |
. . . . . . . . . . . . . 14
⊢ ¬
1o ∈ 1o |
| 20 | | 1oex 8516 |
. . . . . . . . . . . . . . 15
⊢
1o ∈ V |
| 21 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (V =
1o → V = 1o) |
| 22 | 20, 21 | eleqtrid 2847 |
. . . . . . . . . . . . . 14
⊢ (V =
1o → 1o ∈ 1o) |
| 23 | 19, 22 | mto 197 |
. . . . . . . . . . . . 13
⊢ ¬ V
= 1o |
| 24 | | inteq 4949 |
. . . . . . . . . . . . . . 15
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∩
∅) |
| 25 | | int0 4962 |
. . . . . . . . . . . . . . 15
⊢ ∩ ∅ = V |
| 26 | 24, 25 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = V) |
| 27 | 26 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o ↔ V =
1o)) |
| 28 | 23, 27 | mtbiri 327 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → ¬ ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o) |
| 29 | 28 | necon2ai 2970 |
. . . . . . . . . . 11
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ≠
∅) |
| 30 | | onint 7810 |
. . . . . . . . . . 11
⊢ (({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ≠ ∅) →
∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) |
| 31 | 18, 29, 30 | sylancr 587 |
. . . . . . . . . 10
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o → ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)}) |
| 32 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o → (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ↔ 1o
∈ {𝑦 ∈ On ∣
𝑥 ∈
(𝑅1‘suc 𝑦)})) |
| 33 | 31, 32 | mpbid 232 |
. . . . . . . . 9
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o → 1o
∈ {𝑦 ∈ On ∣
𝑥 ∈
(𝑅1‘suc 𝑦)}) |
| 34 | | suceq 6450 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 1o → suc
𝑦 = suc
1o) |
| 35 | 34 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1o →
(𝑅1‘suc 𝑦) = (𝑅1‘suc
1o)) |
| 36 | | df-1o 8506 |
. . . . . . . . . . . . . . . . 17
⊢
1o = suc ∅ |
| 37 | 36 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(𝑅1‘1o) =
(𝑅1‘suc ∅) |
| 38 | | 0elon 6438 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ On |
| 39 | | r1suc 9810 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ On → (𝑅1‘suc ∅) = 𝒫
(𝑅1‘∅)) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(𝑅1‘suc ∅) = 𝒫
(𝑅1‘∅) |
| 41 | | r10 9808 |
. . . . . . . . . . . . . . . . 17
⊢
(𝑅1‘∅) = ∅ |
| 42 | 41 | pweqi 4616 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
(𝑅1‘∅) = 𝒫 ∅ |
| 43 | 37, 40, 42 | 3eqtri 2769 |
. . . . . . . . . . . . . . 15
⊢
(𝑅1‘1o) = 𝒫
∅ |
| 44 | 43 | pweqi 4616 |
. . . . . . . . . . . . . 14
⊢ 𝒫
(𝑅1‘1o) = 𝒫 𝒫
∅ |
| 45 | | pw0 4812 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
∅ = {∅} |
| 46 | 45 | pweqi 4616 |
. . . . . . . . . . . . . 14
⊢ 𝒫
𝒫 ∅ = 𝒫 {∅} |
| 47 | | pwpw0 4813 |
. . . . . . . . . . . . . 14
⊢ 𝒫
{∅} = {∅, {∅}} |
| 48 | 44, 46, 47 | 3eqtrri 2770 |
. . . . . . . . . . . . 13
⊢ {∅,
{∅}} = 𝒫
(𝑅1‘1o) |
| 49 | | 1on 8518 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
| 50 | | r1suc 9810 |
. . . . . . . . . . . . . 14
⊢
(1o ∈ On → (𝑅1‘suc
1o) = 𝒫
(𝑅1‘1o)) |
| 51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(𝑅1‘suc 1o) = 𝒫
(𝑅1‘1o) |
| 52 | 48, 51 | eqtr4i 2768 |
. . . . . . . . . . . 12
⊢ {∅,
{∅}} = (𝑅1‘suc 1o) |
| 53 | 35, 52 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑦 = 1o →
(𝑅1‘suc 𝑦) = {∅, {∅}}) |
| 54 | 53 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑦 = 1o → (𝑥 ∈
(𝑅1‘suc 𝑦) ↔ 𝑥 ∈ {∅,
{∅}})) |
| 55 | 54 | elrab 3692 |
. . . . . . . . 9
⊢
(1o ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ↔ (1o
∈ On ∧ 𝑥 ∈
{∅, {∅}})) |
| 56 | 33, 55 | sylib 218 |
. . . . . . . 8
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o → (1o
∈ On ∧ 𝑥 ∈
{∅, {∅}})) |
| 57 | 12 | elpr 4650 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {∅, {∅}}
↔ (𝑥 = ∅ ∨
𝑥 =
{∅})) |
| 58 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
| 59 | | orel1 889 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅})) |
| 60 | 58, 59 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅})) |
| 61 | | df1o2 8513 |
. . . . . . . . . . . . 13
⊢
1o = {∅} |
| 62 | | eqeq2 2749 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {∅} →
(1o = 𝑥 ↔
1o = {∅})) |
| 63 | 61, 62 | mpbiri 258 |
. . . . . . . . . . . 12
⊢ (𝑥 = {∅} →
1o = 𝑥) |
| 64 | 63 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝑥 = {∅} → 𝑥 =
1o) |
| 65 | 60, 64 | syl6com 37 |
. . . . . . . . . 10
⊢ ((𝑥 = ∅ ∨ 𝑥 = {∅}) → (𝑥 ≠ ∅ → 𝑥 =
1o)) |
| 66 | 57, 65 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑥 ∈ {∅, {∅}}
→ (𝑥 ≠ ∅
→ 𝑥 =
1o)) |
| 67 | 66 | adantl 481 |
. . . . . . . 8
⊢
((1o ∈ On ∧ 𝑥 ∈ {∅, {∅}}) → (𝑥 ≠ ∅ → 𝑥 =
1o)) |
| 68 | 56, 67 | syl 17 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1o → (𝑥 ≠ ∅ → 𝑥 = 1o)) |
| 69 | 17, 68 | sylbi 217 |
. . . . . 6
⊢
((rank‘𝑥) =
1o → (𝑥
≠ ∅ → 𝑥 =
1o)) |
| 70 | 15, 69 | mpd 15 |
. . . . 5
⊢
((rank‘𝑥) =
1o → 𝑥 =
1o) |
| 71 | 9, 70 | vtoclg 3554 |
. . . 4
⊢ (𝐴 ∈ V →
((rank‘𝐴) =
1o → 𝐴 =
1o)) |
| 72 | 6, 71 | mpcom 38 |
. . 3
⊢
((rank‘𝐴) =
1o → 𝐴 =
1o) |
| 73 | | fveq2 6906 |
. . . 4
⊢ (𝐴 = 1o →
(rank‘𝐴) =
(rank‘1o)) |
| 74 | | r111 9815 |
. . . . . . 7
⊢
𝑅1:On–1-1→V |
| 75 | | f1dm 6808 |
. . . . . . 7
⊢
(𝑅1:On–1-1→V → dom 𝑅1 =
On) |
| 76 | 74, 75 | ax-mp 5 |
. . . . . 6
⊢ dom
𝑅1 = On |
| 77 | 49, 76 | eleqtrri 2840 |
. . . . 5
⊢
1o ∈ dom 𝑅1 |
| 78 | | rankonid 9869 |
. . . . 5
⊢
(1o ∈ dom 𝑅1 ↔
(rank‘1o) = 1o) |
| 79 | 77, 78 | mpbi 230 |
. . . 4
⊢
(rank‘1o) = 1o |
| 80 | 73, 79 | eqtrdi 2793 |
. . 3
⊢ (𝐴 = 1o →
(rank‘𝐴) =
1o) |
| 81 | 72, 80 | impbii 209 |
. 2
⊢
((rank‘𝐴) =
1o ↔ 𝐴 =
1o) |
| 82 | 61 | eqeq2i 2750 |
. 2
⊢ (𝐴 = 1o ↔ 𝐴 = {∅}) |
| 83 | 81, 82 | bitri 275 |
1
⊢
((rank‘𝐴) =
1o ↔ 𝐴 =
{∅}) |