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 31250
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 7435 . . . . . . 7 1𝑜 ≠ ∅
2 neeq1 2839 . . . . . . 7 ((rank‘𝐴) = 1𝑜 → ((rank‘𝐴) ≠ ∅ ↔ 1𝑜 ≠ ∅))
31, 2mpbiri 246 . . . . . 6 ((rank‘𝐴) = 1𝑜 → (rank‘𝐴) ≠ ∅)
43neneqd 2782 . . . . 5 ((rank‘𝐴) = 1𝑜 → ¬ (rank‘𝐴) = ∅)
5 fvprc 6078 . . . . 5 𝐴 ∈ V → (rank‘𝐴) = ∅)
64, 5nsyl2 140 . . . 4 ((rank‘𝐴) = 1𝑜𝐴 ∈ V)
7 fveq2 6084 . . . . . . 7 (𝑥 = 𝐴 → (rank‘𝑥) = (rank‘𝐴))
87eqeq1d 2607 . . . . . 6 (𝑥 = 𝐴 → ((rank‘𝑥) = 1𝑜 ↔ (rank‘𝐴) = 1𝑜))
9 eqeq1 2609 . . . . . 6 (𝑥 = 𝐴 → (𝑥 = 1𝑜𝐴 = 1𝑜))
108, 9imbi12d 332 . . . . 5 (𝑥 = 𝐴 → (((rank‘𝑥) = 1𝑜𝑥 = 1𝑜) ↔ ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)))
11 neeq1 2839 . . . . . . . 8 ((rank‘𝑥) = 1𝑜 → ((rank‘𝑥) ≠ ∅ ↔ 1𝑜 ≠ ∅))
121, 11mpbiri 246 . . . . . . 7 ((rank‘𝑥) = 1𝑜 → (rank‘𝑥) ≠ ∅)
13 vex 3171 . . . . . . . . 9 𝑥 ∈ V
1413rankeq0 8580 . . . . . . . 8 (𝑥 = ∅ ↔ (rank‘𝑥) = ∅)
1514necon3bii 2829 . . . . . . 7 (𝑥 ≠ ∅ ↔ (rank‘𝑥) ≠ ∅)
1612, 15sylibr 222 . . . . . 6 ((rank‘𝑥) = 1𝑜𝑥 ≠ ∅)
1713rankval 8535 . . . . . . . 8 (rank‘𝑥) = {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
1817eqeq1i 2610 . . . . . . 7 ((rank‘𝑥) = 1𝑜 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜)
19 ssrab2 3645 . . . . . . . . . . 11 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ⊆ On
20 elirr 8361 . . . . . . . . . . . . . 14 ¬ 1𝑜 ∈ 1𝑜
21 df1o2 7432 . . . . . . . . . . . . . . . 16 1𝑜 = {∅}
22 p0ex 4770 . . . . . . . . . . . . . . . 16 {∅} ∈ V
2321, 22eqeltri 2679 . . . . . . . . . . . . . . 15 1𝑜 ∈ V
24 id 22 . . . . . . . . . . . . . . 15 (V = 1𝑜 → V = 1𝑜)
2523, 24syl5eleq 2689 . . . . . . . . . . . . . 14 (V = 1𝑜 → 1𝑜 ∈ 1𝑜)
2620, 25mto 186 . . . . . . . . . . . . 13 ¬ V = 1𝑜
27 inteq 4403 . . . . . . . . . . . . . . 15 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅)
28 int0 4415 . . . . . . . . . . . . . . 15 ∅ = V
2927, 28syl6eq 2655 . . . . . . . . . . . . . 14 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = V)
3029eqeq1d 2607 . . . . . . . . . . . . 13 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 ↔ V = 1𝑜))
3126, 30mtbiri 315 . . . . . . . . . . . 12 ({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = ∅ → ¬ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜)
3231necon2ai 2806 . . . . . . . . . . 11 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ≠ ∅)
33 onint 6860 . . . . . . . . . . 11 (({𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ≠ ∅) → {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
3419, 32, 33sylancr 693 . . . . . . . . . 10 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
35 eleq1 2671 . . . . . . . . . 10 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ↔ 1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}))
3634, 35mpbid 220 . . . . . . . . 9 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → 1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
37 suceq 5689 . . . . . . . . . . . . 13 (𝑦 = 1𝑜 → suc 𝑦 = suc 1𝑜)
3837fveq2d 6088 . . . . . . . . . . . 12 (𝑦 = 1𝑜 → (𝑅1‘suc 𝑦) = (𝑅1‘suc 1𝑜))
39 df-1o 7420 . . . . . . . . . . . . . . . . 17 1𝑜 = suc ∅
4039fveq2i 6087 . . . . . . . . . . . . . . . 16 (𝑅1‘1𝑜) = (𝑅1‘suc ∅)
41 0elon 5677 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
42 r1suc 8489 . . . . . . . . . . . . . . . . 17 (∅ ∈ On → (𝑅1‘suc ∅) = 𝒫 (𝑅1‘∅))
4341, 42ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑅1‘suc ∅) = 𝒫 (𝑅1‘∅)
44 r10 8487 . . . . . . . . . . . . . . . . 17 (𝑅1‘∅) = ∅
4544pweqi 4107 . . . . . . . . . . . . . . . 16 𝒫 (𝑅1‘∅) = 𝒫 ∅
4640, 43, 453eqtri 2631 . . . . . . . . . . . . . . 15 (𝑅1‘1𝑜) = 𝒫 ∅
4746pweqi 4107 . . . . . . . . . . . . . 14 𝒫 (𝑅1‘1𝑜) = 𝒫 𝒫 ∅
48 pw0 4278 . . . . . . . . . . . . . . 15 𝒫 ∅ = {∅}
4948pweqi 4107 . . . . . . . . . . . . . 14 𝒫 𝒫 ∅ = 𝒫 {∅}
50 pwpw0 4279 . . . . . . . . . . . . . 14 𝒫 {∅} = {∅, {∅}}
5147, 49, 503eqtrri 2632 . . . . . . . . . . . . 13 {∅, {∅}} = 𝒫 (𝑅1‘1𝑜)
52 1on 7427 . . . . . . . . . . . . . 14 1𝑜 ∈ On
53 r1suc 8489 . . . . . . . . . . . . . 14 (1𝑜 ∈ On → (𝑅1‘suc 1𝑜) = 𝒫 (𝑅1‘1𝑜))
5452, 53ax-mp 5 . . . . . . . . . . . . 13 (𝑅1‘suc 1𝑜) = 𝒫 (𝑅1‘1𝑜)
5551, 54eqtr4i 2630 . . . . . . . . . . . 12 {∅, {∅}} = (𝑅1‘suc 1𝑜)
5638, 55syl6eqr 2657 . . . . . . . . . . 11 (𝑦 = 1𝑜 → (𝑅1‘suc 𝑦) = {∅, {∅}})
5756eleq2d 2668 . . . . . . . . . 10 (𝑦 = 1𝑜 → (𝑥 ∈ (𝑅1‘suc 𝑦) ↔ 𝑥 ∈ {∅, {∅}}))
5857elrab 3326 . . . . . . . . 9 (1𝑜 ∈ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} ↔ (1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}))
5936, 58sylib 206 . . . . . . . 8 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → (1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}))
6013elpr 4141 . . . . . . . . . 10 (𝑥 ∈ {∅, {∅}} ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))
61 df-ne 2777 . . . . . . . . . . . 12 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
62 orel1 395 . . . . . . . . . . . 12 𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅}))
6361, 62sylbi 205 . . . . . . . . . . 11 (𝑥 ≠ ∅ → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → 𝑥 = {∅}))
64 eqeq2 2616 . . . . . . . . . . . . 13 (𝑥 = {∅} → (1𝑜 = 𝑥 ↔ 1𝑜 = {∅}))
6521, 64mpbiri 246 . . . . . . . . . . . 12 (𝑥 = {∅} → 1𝑜 = 𝑥)
6665eqcomd 2611 . . . . . . . . . . 11 (𝑥 = {∅} → 𝑥 = 1𝑜)
6763, 66syl6com 36 . . . . . . . . . 10 ((𝑥 = ∅ ∨ 𝑥 = {∅}) → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
6860, 67sylbi 205 . . . . . . . . 9 (𝑥 ∈ {∅, {∅}} → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
6968adantl 480 . . . . . . . 8 ((1𝑜 ∈ On ∧ 𝑥 ∈ {∅, {∅}}) → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
7059, 69syl 17 . . . . . . 7 ( {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} = 1𝑜 → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
7118, 70sylbi 205 . . . . . 6 ((rank‘𝑥) = 1𝑜 → (𝑥 ≠ ∅ → 𝑥 = 1𝑜))
7216, 71mpd 15 . . . . 5 ((rank‘𝑥) = 1𝑜𝑥 = 1𝑜)
7310, 72vtoclg 3234 . . . 4 (𝐴 ∈ V → ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜))
746, 73mpcom 37 . . 3 ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)
75 fveq2 6084 . . . 4 (𝐴 = 1𝑜 → (rank‘𝐴) = (rank‘1𝑜))
76 r111 8494 . . . . . . 7 𝑅1:On–1-1→V
77 f1dm 5999 . . . . . . 7 (𝑅1:On–1-1→V → dom 𝑅1 = On)
7876, 77ax-mp 5 . . . . . 6 dom 𝑅1 = On
7952, 78eleqtrri 2682 . . . . 5 1𝑜 ∈ dom 𝑅1
80 rankonid 8548 . . . . 5 (1𝑜 ∈ dom 𝑅1 ↔ (rank‘1𝑜) = 1𝑜)
8179, 80mpbi 218 . . . 4 (rank‘1𝑜) = 1𝑜
8275, 81syl6eq 2655 . . 3 (𝐴 = 1𝑜 → (rank‘𝐴) = 1𝑜)
8374, 82impbii 197 . 2 ((rank‘𝐴) = 1𝑜𝐴 = 1𝑜)
8421eqeq2i 2617 . 2 (𝐴 = 1𝑜𝐴 = {∅})
8583, 84bitri 262 1 ((rank‘𝐴) = 1𝑜𝐴 = {∅})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1975  wne 2775  {crab 2895  Vcvv 3168  wss 3535  c0 3869  𝒫 cpw 4103  {csn 4120  {cpr 4122   cint 4400  dom cdm 5024  Oncon0 5622  suc csuc 5624  1-1wf1 5783  cfv 5786  1𝑜c1o 7413  𝑅1cr1 8481  rankcrnk 8482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-reg 8353  ax-inf2 8394
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-om 6931  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-er 7602  df-en 7815  df-dom 7816  df-sdom 7817  df-r1 8483  df-rank 8484
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator