Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rankr1c Structured version   Visualization version   GIF version

Theorem rankr1c 9252
 Description: A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
rankr1c (𝐴 (𝑅1 “ On) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵))))

Proof of Theorem rankr1c
StepHypRef Expression
1 id 22 . . . 4 (𝐵 = (rank‘𝐴) → 𝐵 = (rank‘𝐴))
2 rankdmr1 9232 . . . 4 (rank‘𝐴) ∈ dom 𝑅1
31, 2eqeltrdi 2898 . . 3 (𝐵 = (rank‘𝐴) → 𝐵 ∈ dom 𝑅1)
43a1i 11 . 2 (𝐴 (𝑅1 “ On) → (𝐵 = (rank‘𝐴) → 𝐵 ∈ dom 𝑅1))
5 elfvdm 6687 . . . . 5 (𝐴 ∈ (𝑅1‘suc 𝐵) → suc 𝐵 ∈ dom 𝑅1)
6 r1funlim 9197 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
76simpri 489 . . . . . 6 Lim dom 𝑅1
8 limsuc 7557 . . . . . 6 (Lim dom 𝑅1 → (𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1))
97, 8ax-mp 5 . . . . 5 (𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1)
105, 9sylibr 237 . . . 4 (𝐴 ∈ (𝑅1‘suc 𝐵) → 𝐵 ∈ dom 𝑅1)
1110adantl 485 . . 3 ((¬ 𝐴 ∈ (𝑅1𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵)) → 𝐵 ∈ dom 𝑅1)
1211a1i 11 . 2 (𝐴 (𝑅1 “ On) → ((¬ 𝐴 ∈ (𝑅1𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵)) → 𝐵 ∈ dom 𝑅1))
13 eqss 3932 . . . 4 (𝐵 = (rank‘𝐴) ↔ (𝐵 ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ⊆ 𝐵))
14 rankr1clem 9251 . . . . 5 ((𝐴 (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1𝐵) ↔ 𝐵 ⊆ (rank‘𝐴)))
15 rankr1ag 9233 . . . . . . 7 ((𝐴 (𝑅1 “ On) ∧ suc 𝐵 ∈ dom 𝑅1) → (𝐴 ∈ (𝑅1‘suc 𝐵) ↔ (rank‘𝐴) ∈ suc 𝐵))
169, 15sylan2b 596 . . . . . 6 ((𝐴 (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ∈ (𝑅1‘suc 𝐵) ↔ (rank‘𝐴) ∈ suc 𝐵))
17 rankon 9226 . . . . . . 7 (rank‘𝐴) ∈ On
18 limord 6225 . . . . . . . . . 10 (Lim dom 𝑅1 → Ord dom 𝑅1)
197, 18ax-mp 5 . . . . . . . . 9 Ord dom 𝑅1
20 ordelon 6190 . . . . . . . . 9 ((Ord dom 𝑅1𝐵 ∈ dom 𝑅1) → 𝐵 ∈ On)
2119, 20mpan 689 . . . . . . . 8 (𝐵 ∈ dom 𝑅1𝐵 ∈ On)
2221adantl 485 . . . . . . 7 ((𝐴 (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → 𝐵 ∈ On)
23 onsssuc 6253 . . . . . . 7 (((rank‘𝐴) ∈ On ∧ 𝐵 ∈ On) → ((rank‘𝐴) ⊆ 𝐵 ↔ (rank‘𝐴) ∈ suc 𝐵))
2417, 22, 23sylancr 590 . . . . . 6 ((𝐴 (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → ((rank‘𝐴) ⊆ 𝐵 ↔ (rank‘𝐴) ∈ suc 𝐵))
2516, 24bitr4d 285 . . . . 5 ((𝐴 (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ∈ (𝑅1‘suc 𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
2614, 25anbi12d 633 . . . 4 ((𝐴 (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → ((¬ 𝐴 ∈ (𝑅1𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵)) ↔ (𝐵 ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ⊆ 𝐵)))
2713, 26bitr4id 293 . . 3 ((𝐴 (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵))))
2827ex 416 . 2 (𝐴 (𝑅1 “ On) → (𝐵 ∈ dom 𝑅1 → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵)))))
294, 12, 28pm5.21ndd 384 1 (𝐴 (𝑅1 “ On) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ⊆ wss 3883  ∪ cuni 4804  dom cdm 5523   “ cima 5526  Ord word 6165  Oncon0 6166  Lim wlim 6167  suc csuc 6168  Fun wfun 6326  ‘cfv 6332  𝑅1cr1 9193  rankcrnk 9194 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-om 7574  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-r1 9195  df-rank 9196 This theorem is referenced by:  rankidn  9253  rankpwi  9254  rankr1g  9263  r1tskina  10211
 Copyright terms: Public domain W3C validator