Step | Hyp | Ref
| Expression |
1 | | 1n0 7462 |
. . . . . . 7
⊢
1𝑜 ≠ ∅ |
2 | | neeq1 2844 |
. . . . . . 7
⊢
((rank‘𝐴) =
1𝑜 → ((rank‘𝐴) ≠ ∅ ↔ 1𝑜
≠ ∅)) |
3 | 1, 2 | mpbiri 247 |
. . . . . 6
⊢
((rank‘𝐴) =
1𝑜 → (rank‘𝐴) ≠ ∅) |
4 | 3 | neneqd 2787 |
. . . . 5
⊢
((rank‘𝐴) =
1𝑜 → ¬ (rank‘𝐴) = ∅) |
5 | | fvprc 6097 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
(rank‘𝐴) =
∅) |
6 | 4, 5 | nsyl2 141 |
. . . 4
⊢
((rank‘𝐴) =
1𝑜 → 𝐴 ∈ V) |
7 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (rank‘𝑥) = (rank‘𝐴)) |
8 | 7 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((rank‘𝑥) = 1𝑜 ↔
(rank‘𝐴) =
1𝑜)) |
9 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 = 1𝑜 ↔ 𝐴 =
1𝑜)) |
10 | 8, 9 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((rank‘𝑥) = 1𝑜 → 𝑥 = 1𝑜) ↔
((rank‘𝐴) =
1𝑜 → 𝐴 = 1𝑜))) |
11 | | neeq1 2844 |
. . . . . . . 8
⊢
((rank‘𝑥) =
1𝑜 → ((rank‘𝑥) ≠ ∅ ↔ 1𝑜
≠ ∅)) |
12 | 1, 11 | mpbiri 247 |
. . . . . . 7
⊢
((rank‘𝑥) =
1𝑜 → (rank‘𝑥) ≠ ∅) |
13 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
14 | 13 | rankeq0 8607 |
. . . . . . . 8
⊢ (𝑥 = ∅ ↔
(rank‘𝑥) =
∅) |
15 | 14 | necon3bii 2834 |
. . . . . . 7
⊢ (𝑥 ≠ ∅ ↔
(rank‘𝑥) ≠
∅) |
16 | 12, 15 | sylibr 223 |
. . . . . 6
⊢
((rank‘𝑥) =
1𝑜 → 𝑥 ≠ ∅) |
17 | 13 | rankval 8562 |
. . . . . . . 8
⊢
(rank‘𝑥) =
∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} |
18 | 17 | eqeq1i 2615 |
. . . . . . 7
⊢
((rank‘𝑥) =
1𝑜 ↔ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} =
1𝑜) |
19 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ⊆ On |
20 | | elirr 8388 |
. . . . . . . . . . . . . 14
⊢ ¬
1𝑜 ∈ 1𝑜 |
21 | | df1o2 7459 |
. . . . . . . . . . . . . . . 16
⊢
1𝑜 = {∅} |
22 | | p0ex 4779 |
. . . . . . . . . . . . . . . 16
⊢ {∅}
∈ V |
23 | 21, 22 | eqeltri 2684 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ∈ V |
24 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (V =
1𝑜 → V = 1𝑜) |
25 | 23, 24 | syl5eleq 2694 |
. . . . . . . . . . . . . 14
⊢ (V =
1𝑜 → 1𝑜 ∈
1𝑜) |
26 | 20, 25 | mto 187 |
. . . . . . . . . . . . 13
⊢ ¬ V
= 1𝑜 |
27 | | inteq 4413 |
. . . . . . . . . . . . . . 15
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∩
∅) |
28 | | int0 4425 |
. . . . . . . . . . . . . . 15
⊢ ∩ ∅ = V |
29 | 27, 28 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = V) |
30 | 29 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜 ↔ V =
1𝑜)) |
31 | 26, 30 | mtbiri 316 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = ∅ → ¬ ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜) |
32 | 31 | necon2ai 2811 |
. . . . . . . . . . 11
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜 → {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ≠ ∅) |
33 | | onint 6887 |
. . . . . . . . . . 11
⊢ (({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ≠ ∅) →
∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) |
34 | 19, 32, 33 | sylancr 694 |
. . . . . . . . . 10
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜 → ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)}) |
35 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜 → (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ↔
1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)})) |
36 | 34, 35 | mpbid 221 |
. . . . . . . . 9
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜 →
1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)}) |
37 | | suceq 5707 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 1𝑜 →
suc 𝑦 = suc
1𝑜) |
38 | 37 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1𝑜 →
(𝑅1‘suc 𝑦) = (𝑅1‘suc
1𝑜)) |
39 | | df-1o 7447 |
. . . . . . . . . . . . . . . . 17
⊢
1𝑜 = suc ∅ |
40 | 39 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(𝑅1‘1𝑜) =
(𝑅1‘suc ∅) |
41 | | 0elon 5695 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ On |
42 | | r1suc 8516 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ On → (𝑅1‘suc ∅) = 𝒫
(𝑅1‘∅)) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(𝑅1‘suc ∅) = 𝒫
(𝑅1‘∅) |
44 | | r10 8514 |
. . . . . . . . . . . . . . . . 17
⊢
(𝑅1‘∅) = ∅ |
45 | 44 | pweqi 4112 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
(𝑅1‘∅) = 𝒫 ∅ |
46 | 40, 43, 45 | 3eqtri 2636 |
. . . . . . . . . . . . . . 15
⊢
(𝑅1‘1𝑜) = 𝒫
∅ |
47 | 46 | pweqi 4112 |
. . . . . . . . . . . . . 14
⊢ 𝒫
(𝑅1‘1𝑜) = 𝒫 𝒫
∅ |
48 | | pw0 4283 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
∅ = {∅} |
49 | 48 | pweqi 4112 |
. . . . . . . . . . . . . 14
⊢ 𝒫
𝒫 ∅ = 𝒫 {∅} |
50 | | pwpw0 4284 |
. . . . . . . . . . . . . 14
⊢ 𝒫
{∅} = {∅, {∅}} |
51 | 47, 49, 50 | 3eqtrri 2637 |
. . . . . . . . . . . . 13
⊢ {∅,
{∅}} = 𝒫
(𝑅1‘1𝑜) |
52 | | 1on 7454 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ On |
53 | | r1suc 8516 |
. . . . . . . . . . . . . 14
⊢
(1𝑜 ∈ On → (𝑅1‘suc
1𝑜) = 𝒫
(𝑅1‘1𝑜)) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(𝑅1‘suc 1𝑜) = 𝒫
(𝑅1‘1𝑜) |
55 | 51, 54 | eqtr4i 2635 |
. . . . . . . . . . . 12
⊢ {∅,
{∅}} = (𝑅1‘suc
1𝑜) |
56 | 38, 55 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑦 = 1𝑜 →
(𝑅1‘suc 𝑦) = {∅, {∅}}) |
57 | 56 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑦 = 1𝑜 →
(𝑥 ∈
(𝑅1‘suc 𝑦) ↔ 𝑥 ∈ {∅,
{∅}})) |
58 | 57 | elrab 3331 |
. . . . . . . . 9
⊢
(1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ↔
(1𝑜 ∈ On ∧ 𝑥 ∈ {∅,
{∅}})) |
59 | 36, 58 | sylib 207 |
. . . . . . . 8
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜 →
(1𝑜 ∈ On ∧ 𝑥 ∈ {∅,
{∅}})) |
60 | 13 | elpr 4146 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {∅, {∅}}
↔ (𝑥 = ∅ ∨
𝑥 =
{∅})) |
61 | | df-ne 2782 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
62 | | orel1 396 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅})) |
63 | 61, 62 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅})) |
64 | | eqeq2 2621 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {∅} →
(1𝑜 = 𝑥
↔ 1𝑜 = {∅})) |
65 | 21, 64 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ (𝑥 = {∅} →
1𝑜 = 𝑥) |
66 | 65 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝑥 = {∅} → 𝑥 =
1𝑜) |
67 | 63, 66 | syl6com 36 |
. . . . . . . . . 10
⊢ ((𝑥 = ∅ ∨ 𝑥 = {∅}) → (𝑥 ≠ ∅ → 𝑥 =
1𝑜)) |
68 | 60, 67 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑥 ∈ {∅, {∅}}
→ (𝑥 ≠ ∅
→ 𝑥 =
1𝑜)) |
69 | 68 | adantl 481 |
. . . . . . . 8
⊢
((1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}) → (𝑥 ≠ ∅ → 𝑥 =
1𝑜)) |
70 | 59, 69 | syl 17 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} = 1𝑜 → (𝑥 ≠ ∅ → 𝑥 =
1𝑜)) |
71 | 18, 70 | sylbi 206 |
. . . . . 6
⊢
((rank‘𝑥) =
1𝑜 → (𝑥 ≠ ∅ → 𝑥 = 1𝑜)) |
72 | 16, 71 | mpd 15 |
. . . . 5
⊢
((rank‘𝑥) =
1𝑜 → 𝑥 = 1𝑜) |
73 | 10, 72 | vtoclg 3239 |
. . . 4
⊢ (𝐴 ∈ V →
((rank‘𝐴) =
1𝑜 → 𝐴 = 1𝑜)) |
74 | 6, 73 | mpcom 37 |
. . 3
⊢
((rank‘𝐴) =
1𝑜 → 𝐴 = 1𝑜) |
75 | | fveq2 6103 |
. . . 4
⊢ (𝐴 = 1𝑜 →
(rank‘𝐴) =
(rank‘1𝑜)) |
76 | | r111 8521 |
. . . . . . 7
⊢
𝑅1:On–1-1→V |
77 | | f1dm 6018 |
. . . . . . 7
⊢
(𝑅1:On–1-1→V → dom 𝑅1 =
On) |
78 | 76, 77 | ax-mp 5 |
. . . . . 6
⊢ dom
𝑅1 = On |
79 | 52, 78 | eleqtrri 2687 |
. . . . 5
⊢
1𝑜 ∈ dom 𝑅1 |
80 | | rankonid 8575 |
. . . . 5
⊢
(1𝑜 ∈ dom 𝑅1 ↔
(rank‘1𝑜) = 1𝑜) |
81 | 79, 80 | mpbi 219 |
. . . 4
⊢
(rank‘1𝑜) =
1𝑜 |
82 | 75, 81 | syl6eq 2660 |
. . 3
⊢ (𝐴 = 1𝑜 →
(rank‘𝐴) =
1𝑜) |
83 | 74, 82 | impbii 198 |
. 2
⊢
((rank‘𝐴) =
1𝑜 ↔ 𝐴 = 1𝑜) |
84 | 21 | eqeq2i 2622 |
. 2
⊢ (𝐴 = 1𝑜 ↔
𝐴 =
{∅}) |
85 | 83, 84 | bitri 263 |
1
⊢
((rank‘𝐴) =
1𝑜 ↔ 𝐴 = {∅}) |