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 32403
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 7620 . . . . . . 7 1𝑜 ≠ ∅
2 neeq1 2885 . . . . . . 7 ((rank‘𝐴) = 1𝑜 → ((rank‘𝐴) ≠ ∅ ↔ 1𝑜 ≠ ∅))
31, 2mpbiri 248 . . . . . 6 ((rank‘𝐴) = 1𝑜 → (rank‘𝐴) ≠ ∅)
43neneqd 2828 . . . . 5 ((rank‘𝐴) = 1𝑜 → ¬ (rank‘𝐴) = ∅)
5 fvprc 6223 . . . . 5 𝐴 ∈ V → (rank‘𝐴) = ∅)
64, 5nsyl2 142 . . . 4 ((rank‘𝐴) = 1𝑜𝐴 ∈ V)
7 fveq2 6229 . . . . . . 7 (𝑥 = 𝐴 → (rank‘𝑥) = (rank‘𝐴))
87eqeq1d 2653 . . . . . 6 (𝑥 = 𝐴 → ((rank‘𝑥) = 1𝑜 ↔ (rank‘𝐴) = 1𝑜))
9 eqeq1 2655 . . . . . 6 (𝑥 = 𝐴 → (𝑥 = 1𝑜𝐴 = 1𝑜))
108, 9imbi12d 333 . . . . 5 (𝑥 = 𝐴 → (((rank‘𝑥) = 1𝑜𝑥 = 1𝑜) ↔ ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)))
11 neeq1 2885 . . . . . . . 8 ((rank‘𝑥) = 1𝑜 → ((rank‘𝑥) ≠ ∅ ↔ 1𝑜 ≠ ∅))
121, 11mpbiri 248 . . . . . . 7 ((rank‘𝑥) = 1𝑜 → (rank‘𝑥) ≠ ∅)
13 vex 3234 . . . . . . . . 9 𝑥 ∈ V
1413rankeq0 8762 . . . . . . . 8 (𝑥 = ∅ ↔ (rank‘𝑥) = ∅)
1514necon3bii 2875 . . . . . . 7 (𝑥 ≠ ∅ ↔ (rank‘𝑥) ≠ ∅)
1612, 15sylibr 224 . . . . . 6 ((rank‘𝑥) = 1𝑜𝑥 ≠ ∅)
1713rankval 8717 . . . . . . . 8 (rank‘𝑥) = {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
1817eqeq1i 2656 . . . . . . 7 ((rank‘𝑥) = 1𝑜 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜)
19 ssrab2 3720 . . . . . . . . . . 11 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ⊆ On
20 elirr 8543 . . . . . . . . . . . . . 14 ¬ 1𝑜 ∈ 1𝑜
21 df1o2 7617 . . . . . . . . . . . . . . . 16 1𝑜 = {∅}
22 p0ex 4883 . . . . . . . . . . . . . . . 16 {∅} ∈ V
2321, 22eqeltri 2726 . . . . . . . . . . . . . . 15 1𝑜 ∈ V
24 id 22 . . . . . . . . . . . . . . 15 (V = 1𝑜 → V = 1𝑜)
2523, 24syl5eleq 2736 . . . . . . . . . . . . . 14 (V = 1𝑜 → 1𝑜 ∈ 1𝑜)
2620, 25mto 188 . . . . . . . . . . . . 13 ¬ V = 1𝑜
27 inteq 4510 . . . . . . . . . . . . . . 15 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅)
28 int0 4522 . . . . . . . . . . . . . . 15 ∅ = V
2927, 28syl6eq 2701 . . . . . . . . . . . . . 14 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = V)
3029eqeq1d 2653 . . . . . . . . . . . . 13 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 ↔ V = 1𝑜))
3126, 30mtbiri 316 . . . . . . . . . . . 12 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → ¬ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜)
3231necon2ai 2852 . . . . . . . . . . 11 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ≠ ∅)
33 onint 7037 . . . . . . . . . . 11 (({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ≠ ∅) → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
3419, 32, 33sylancr 696 . . . . . . . . . 10 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
35 eleq1 2718 . . . . . . . . . 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 5828 . . . . . . . . . . . . 13 (𝑦 = 1𝑜 → suc 𝑦 = suc 1𝑜)
3837fveq2d 6233 . . . . . . . . . . . 12 (𝑦 = 1𝑜 → (𝑅1‘suc 𝑦) = (𝑅1‘suc 1𝑜))
39 df-1o 7605 . . . . . . . . . . . . . . . . 17 1𝑜 = suc ∅
4039fveq2i 6232 . . . . . . . . . . . . . . . 16 (𝑅1‘1𝑜) = (𝑅1‘suc ∅)
41 0elon 5816 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
42 r1suc 8671 . . . . . . . . . . . . . . . . 17 (∅ ∈ On → (𝑅1‘suc ∅) = 𝒫 (𝑅1‘∅))
4341, 42ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑅1‘suc ∅) = 𝒫 (𝑅1‘∅)
44 r10 8669 . . . . . . . . . . . . . . . . 17 (𝑅1‘∅) = ∅
4544pweqi 4195 . . . . . . . . . . . . . . . 16 𝒫 (𝑅1‘∅) = 𝒫 ∅
4640, 43, 453eqtri 2677 . . . . . . . . . . . . . . 15 (𝑅1‘1𝑜) = 𝒫 ∅
4746pweqi 4195 . . . . . . . . . . . . . 14 𝒫 (𝑅1‘1𝑜) = 𝒫 𝒫 ∅
48 pw0 4375 . . . . . . . . . . . . . . 15 𝒫 ∅ = {∅}
4948pweqi 4195 . . . . . . . . . . . . . 14 𝒫 𝒫 ∅ = 𝒫 {∅}
50 pwpw0 4376 . . . . . . . . . . . . . 14 𝒫 {∅} = {∅, {∅}}
5147, 49, 503eqtrri 2678 . . . . . . . . . . . . 13 {∅, {∅}} = 𝒫 (𝑅1‘1𝑜)
52 1on 7612 . . . . . . . . . . . . . 14 1𝑜 ∈ On
53 r1suc 8671 . . . . . . . . . . . . . 14 (1𝑜 ∈ On → (𝑅1‘suc 1𝑜) = 𝒫 (𝑅1‘1𝑜))
5452, 53ax-mp 5 . . . . . . . . . . . . 13 (𝑅1‘suc 1𝑜) = 𝒫 (𝑅1‘1𝑜)
5551, 54eqtr4i 2676 . . . . . . . . . . . 12 {∅, {∅}} = (𝑅1‘suc 1𝑜)
5638, 55syl6eqr 2703 . . . . . . . . . . 11 (𝑦 = 1𝑜 → (𝑅1‘suc 𝑦) = {∅, {∅}})
5756eleq2d 2716 . . . . . . . . . 10 (𝑦 = 1𝑜 → (𝑥 ∈ (𝑅1‘suc 𝑦) ↔ 𝑥 ∈ {∅, {∅}}))
5857elrab 3396 . . . . . . . . 9 (1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ↔ (1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}))
5936, 58sylib 208 . . . . . . . 8 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → (1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}))
6013elpr 4231 . . . . . . . . . 10 (𝑥 ∈ {∅, {∅}} ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))
61 df-ne 2824 . . . . . . . . . . . 12 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
62 orel1 396 . . . . . . . . . . . 12 𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅}))
6361, 62sylbi 207 . . . . . . . . . . 11 (𝑥 ≠ ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅}))
64 eqeq2 2662 . . . . . . . . . . . . 13 (𝑥 = {∅} → (1𝑜 = 𝑥 ↔ 1𝑜 = {∅}))
6521, 64mpbiri 248 . . . . . . . . . . . 12 (𝑥 = {∅} → 1𝑜 = 𝑥)
6665eqcomd 2657 . . . . . . . . . . 11 (𝑥 = {∅} → 𝑥 = 1𝑜)
6763, 66syl6com 37 . . . . . . . . . 10 ((𝑥 = ∅ ∨ 𝑥 = {∅}) → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
6860, 67sylbi 207 . . . . . . . . 9 (𝑥 ∈ {∅, {∅}} → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
6968adantl 481 . . . . . . . 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 3297 . . . 4 (𝐴 ∈ V → ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜))
746, 73mpcom 38 . . 3 ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)
75 fveq2 6229 . . . 4 (𝐴 = 1𝑜 → (rank‘𝐴) = (rank‘1𝑜))
76 r111 8676 . . . . . . 7 𝑅1:On–1-1→V
77 f1dm 6143 . . . . . . 7 (𝑅1:On–1-1→V → dom 𝑅1 = On)
7876, 77ax-mp 5 . . . . . 6 dom 𝑅1 = On
7952, 78eleqtrri 2729 . . . . 5 1𝑜 ∈ dom 𝑅1
80 rankonid 8730 . . . . 5 (1𝑜 ∈ dom 𝑅1 ↔ (rank‘1𝑜) = 1𝑜)
8179, 80mpbi 220 . . . 4 (rank‘1𝑜) = 1𝑜
8275, 81syl6eq 2701 . . 3 (𝐴 = 1𝑜 → (rank‘𝐴) = 1𝑜)
8374, 82impbii 199 . 2 ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)
8421eqeq2i 2663 . 2 (𝐴 = 1𝑜𝐴 = {∅})
8583, 84bitri 264 1 ((rank‘𝐴) = 1𝑜𝐴 = {∅})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  wne 2823  {crab 2945  Vcvv 3231  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210  {cpr 4212   cint 4507  dom cdm 5143  Oncon0 5761  suc csuc 5763  1-1wf1 5923  cfv 5926  1𝑜c1o 7598  𝑅1cr1 8663  rankcrnk 8664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-reg 8538  ax-inf2 8576
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-r1 8665  df-rank 8666
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator