Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rankeq1o Structured version   Visualization version   GIF version

Theorem rankeq1o 32253
Description: The only set with rank 1𝑜 is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.)
Assertion
Ref Expression
rankeq1o ((rank‘𝐴) = 1𝑜𝐴 = {∅})

Proof of Theorem rankeq1o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1n0 7560 . . . . . . 7 1𝑜 ≠ ∅
2 neeq1 2853 . . . . . . 7 ((rank‘𝐴) = 1𝑜 → ((rank‘𝐴) ≠ ∅ ↔ 1𝑜 ≠ ∅))
31, 2mpbiri 248 . . . . . 6 ((rank‘𝐴) = 1𝑜 → (rank‘𝐴) ≠ ∅)
43neneqd 2796 . . . . 5 ((rank‘𝐴) = 1𝑜 → ¬ (rank‘𝐴) = ∅)
5 fvprc 6172 . . . . 5 𝐴 ∈ V → (rank‘𝐴) = ∅)
64, 5nsyl2 142 . . . 4 ((rank‘𝐴) = 1𝑜𝐴 ∈ V)
7 fveq2 6178 . . . . . . 7 (𝑥 = 𝐴 → (rank‘𝑥) = (rank‘𝐴))
87eqeq1d 2622 . . . . . 6 (𝑥 = 𝐴 → ((rank‘𝑥) = 1𝑜 ↔ (rank‘𝐴) = 1𝑜))
9 eqeq1 2624 . . . . . 6 (𝑥 = 𝐴 → (𝑥 = 1𝑜𝐴 = 1𝑜))
108, 9imbi12d 334 . . . . 5 (𝑥 = 𝐴 → (((rank‘𝑥) = 1𝑜𝑥 = 1𝑜) ↔ ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)))
11 neeq1 2853 . . . . . . . 8 ((rank‘𝑥) = 1𝑜 → ((rank‘𝑥) ≠ ∅ ↔ 1𝑜 ≠ ∅))
121, 11mpbiri 248 . . . . . . 7 ((rank‘𝑥) = 1𝑜 → (rank‘𝑥) ≠ ∅)
13 vex 3198 . . . . . . . . 9 𝑥 ∈ V
1413rankeq0 8709 . . . . . . . 8 (𝑥 = ∅ ↔ (rank‘𝑥) = ∅)
1514necon3bii 2843 . . . . . . 7 (𝑥 ≠ ∅ ↔ (rank‘𝑥) ≠ ∅)
1612, 15sylibr 224 . . . . . 6 ((rank‘𝑥) = 1𝑜𝑥 ≠ ∅)
1713rankval 8664 . . . . . . . 8 (rank‘𝑥) = {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
1817eqeq1i 2625 . . . . . . 7 ((rank‘𝑥) = 1𝑜 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜)
19 ssrab2 3679 . . . . . . . . . . 11 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ⊆ On
20 elirr 8490 . . . . . . . . . . . . . 14 ¬ 1𝑜 ∈ 1𝑜
21 df1o2 7557 . . . . . . . . . . . . . . . 16 1𝑜 = {∅}
22 p0ex 4844 . . . . . . . . . . . . . . . 16 {∅} ∈ V
2321, 22eqeltri 2695 . . . . . . . . . . . . . . 15 1𝑜 ∈ V
24 id 22 . . . . . . . . . . . . . . 15 (V = 1𝑜 → V = 1𝑜)
2523, 24syl5eleq 2705 . . . . . . . . . . . . . 14 (V = 1𝑜 → 1𝑜 ∈ 1𝑜)
2620, 25mto 188 . . . . . . . . . . . . 13 ¬ V = 1𝑜
27 inteq 4469 . . . . . . . . . . . . . . 15 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅)
28 int0 4481 . . . . . . . . . . . . . . 15 ∅ = V
2927, 28syl6eq 2670 . . . . . . . . . . . . . 14 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = V)
3029eqeq1d 2622 . . . . . . . . . . . . 13 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 ↔ V = 1𝑜))
3126, 30mtbiri 317 . . . . . . . . . . . 12 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → ¬ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜)
3231necon2ai 2820 . . . . . . . . . . 11 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ≠ ∅)
33 onint 6980 . . . . . . . . . . 11 (({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ≠ ∅) → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
3419, 32, 33sylancr 694 . . . . . . . . . 10 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
35 eleq1 2687 . . . . . . . . . 10 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ↔ 1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}))
3634, 35mpbid 222 . . . . . . . . 9 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → 1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
37 suceq 5778 . . . . . . . . . . . . 13 (𝑦 = 1𝑜 → suc 𝑦 = suc 1𝑜)
3837fveq2d 6182 . . . . . . . . . . . 12 (𝑦 = 1𝑜 → (𝑅1‘suc 𝑦) = (𝑅1‘suc 1𝑜))
39 df-1o 7545 . . . . . . . . . . . . . . . . 17 1𝑜 = suc ∅
4039fveq2i 6181 . . . . . . . . . . . . . . . 16 (𝑅1‘1𝑜) = (𝑅1‘suc ∅)
41 0elon 5766 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
42 r1suc 8618 . . . . . . . . . . . . . . . . 17 (∅ ∈ On → (𝑅1‘suc ∅) = 𝒫 (𝑅1‘∅))
4341, 42ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑅1‘suc ∅) = 𝒫 (𝑅1‘∅)
44 r10 8616 . . . . . . . . . . . . . . . . 17 (𝑅1‘∅) = ∅
4544pweqi 4153 . . . . . . . . . . . . . . . 16 𝒫 (𝑅1‘∅) = 𝒫 ∅
4640, 43, 453eqtri 2646 . . . . . . . . . . . . . . 15 (𝑅1‘1𝑜) = 𝒫 ∅
4746pweqi 4153 . . . . . . . . . . . . . 14 𝒫 (𝑅1‘1𝑜) = 𝒫 𝒫 ∅
48 pw0 4334 . . . . . . . . . . . . . . 15 𝒫 ∅ = {∅}
4948pweqi 4153 . . . . . . . . . . . . . 14 𝒫 𝒫 ∅ = 𝒫 {∅}
50 pwpw0 4335 . . . . . . . . . . . . . 14 𝒫 {∅} = {∅, {∅}}
5147, 49, 503eqtrri 2647 . . . . . . . . . . . . 13 {∅, {∅}} = 𝒫 (𝑅1‘1𝑜)
52 1on 7552 . . . . . . . . . . . . . 14 1𝑜 ∈ On
53 r1suc 8618 . . . . . . . . . . . . . 14 (1𝑜 ∈ On → (𝑅1‘suc 1𝑜) = 𝒫 (𝑅1‘1𝑜))
5452, 53ax-mp 5 . . . . . . . . . . . . 13 (𝑅1‘suc 1𝑜) = 𝒫 (𝑅1‘1𝑜)
5551, 54eqtr4i 2645 . . . . . . . . . . . 12 {∅, {∅}} = (𝑅1‘suc 1𝑜)
5638, 55syl6eqr 2672 . . . . . . . . . . 11 (𝑦 = 1𝑜 → (𝑅1‘suc 𝑦) = {∅, {∅}})
5756eleq2d 2685 . . . . . . . . . 10 (𝑦 = 1𝑜 → (𝑥 ∈ (𝑅1‘suc 𝑦) ↔ 𝑥 ∈ {∅, {∅}}))
5857elrab 3357 . . . . . . . . 9 (1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ↔ (1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}))
5936, 58sylib 208 . . . . . . . 8 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → (1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}))
6013elpr 4189 . . . . . . . . . 10 (𝑥 ∈ {∅, {∅}} ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))
61 df-ne 2792 . . . . . . . . . . . 12 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
62 orel1 397 . . . . . . . . . . . 12 𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅}))
6361, 62sylbi 207 . . . . . . . . . . 11 (𝑥 ≠ ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅}))
64 eqeq2 2631 . . . . . . . . . . . . 13 (𝑥 = {∅} → (1𝑜 = 𝑥 ↔ 1𝑜 = {∅}))
6521, 64mpbiri 248 . . . . . . . . . . . 12 (𝑥 = {∅} → 1𝑜 = 𝑥)
6665eqcomd 2626 . . . . . . . . . . 11 (𝑥 = {∅} → 𝑥 = 1𝑜)
6763, 66syl6com 37 . . . . . . . . . 10 ((𝑥 = ∅ ∨ 𝑥 = {∅}) → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
6860, 67sylbi 207 . . . . . . . . 9 (𝑥 ∈ {∅, {∅}} → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
6968adantl 482 . . . . . . . 8 ((1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}) → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
7059, 69syl 17 . . . . . . 7 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
7118, 70sylbi 207 . . . . . 6 ((rank‘𝑥) = 1𝑜 → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
7216, 71mpd 15 . . . . 5 ((rank‘𝑥) = 1𝑜𝑥 = 1𝑜)
7310, 72vtoclg 3261 . . . 4 (𝐴 ∈ V → ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜))
746, 73mpcom 38 . . 3 ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)
75 fveq2 6178 . . . 4 (𝐴 = 1𝑜 → (rank‘𝐴) = (rank‘1𝑜))
76 r111 8623 . . . . . . 7 𝑅1:On–1-1→V
77 f1dm 6092 . . . . . . 7 (𝑅1:On–1-1→V → dom 𝑅1 = On)
7876, 77ax-mp 5 . . . . . 6 dom 𝑅1 = On
7952, 78eleqtrri 2698 . . . . 5 1𝑜 ∈ dom 𝑅1
80 rankonid 8677 . . . . 5 (1𝑜 ∈ dom 𝑅1 ↔ (rank‘1𝑜) = 1𝑜)
8179, 80mpbi 220 . . . 4 (rank‘1𝑜) = 1𝑜
8275, 81syl6eq 2670 . . 3 (𝐴 = 1𝑜 → (rank‘𝐴) = 1𝑜)
8374, 82impbii 199 . 2 ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)
8421eqeq2i 2632 . 2 (𝐴 = 1𝑜𝐴 = {∅})
8583, 84bitri 264 1 ((rank‘𝐴) = 1𝑜𝐴 = {∅})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1481  wcel 1988  wne 2791  {crab 2913  Vcvv 3195  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168  {cpr 4170   cint 4466  dom cdm 5104  Oncon0 5711  suc csuc 5713  1-1wf1 5873  cfv 5876  1𝑜c1o 7538  𝑅1cr1 8610  rankcrnk 8611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-reg 8482  ax-inf2 8523
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-r1 8612  df-rank 8613
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator