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

Theorem rankr1ai 8938
Description: One direction of rankr1a 8976. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
rankr1ai (𝐴 ∈ (𝑅1𝐵) → (rank‘𝐴) ∈ 𝐵)

Proof of Theorem rankr1ai
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elfvdm 6465 . . 3 (𝐴 ∈ (𝑅1𝐵) → 𝐵 ∈ dom 𝑅1)
2 r1val1 8926 . . . . . 6 (𝐵 ∈ dom 𝑅1 → (𝑅1𝐵) = 𝑥𝐵 𝒫 (𝑅1𝑥))
32eleq2d 2892 . . . . 5 (𝐵 ∈ dom 𝑅1 → (𝐴 ∈ (𝑅1𝐵) ↔ 𝐴 𝑥𝐵 𝒫 (𝑅1𝑥)))
4 eliun 4744 . . . . 5 (𝐴 𝑥𝐵 𝒫 (𝑅1𝑥) ↔ ∃𝑥𝐵 𝐴 ∈ 𝒫 (𝑅1𝑥))
53, 4syl6bb 279 . . . 4 (𝐵 ∈ dom 𝑅1 → (𝐴 ∈ (𝑅1𝐵) ↔ ∃𝑥𝐵 𝐴 ∈ 𝒫 (𝑅1𝑥)))
6 r1funlim 8906 . . . . . . . . . . 11 (Fun 𝑅1 ∧ Lim dom 𝑅1)
76simpri 481 . . . . . . . . . 10 Lim dom 𝑅1
8 limord 6022 . . . . . . . . . 10 (Lim dom 𝑅1 → Ord dom 𝑅1)
97, 8ax-mp 5 . . . . . . . . 9 Ord dom 𝑅1
10 ordtr1 6006 . . . . . . . . 9 (Ord dom 𝑅1 → ((𝑥𝐵𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1))
119, 10ax-mp 5 . . . . . . . 8 ((𝑥𝐵𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1)
1211ancoms 452 . . . . . . 7 ((𝐵 ∈ dom 𝑅1𝑥𝐵) → 𝑥 ∈ dom 𝑅1)
13 r1sucg 8909 . . . . . . . 8 (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
1413eleq2d 2892 . . . . . . 7 (𝑥 ∈ dom 𝑅1 → (𝐴 ∈ (𝑅1‘suc 𝑥) ↔ 𝐴 ∈ 𝒫 (𝑅1𝑥)))
1512, 14syl 17 . . . . . 6 ((𝐵 ∈ dom 𝑅1𝑥𝐵) → (𝐴 ∈ (𝑅1‘suc 𝑥) ↔ 𝐴 ∈ 𝒫 (𝑅1𝑥)))
16 ordsson 7250 . . . . . . . . . 10 (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
179, 16ax-mp 5 . . . . . . . . 9 dom 𝑅1 ⊆ On
1817, 12sseldi 3825 . . . . . . . 8 ((𝐵 ∈ dom 𝑅1𝑥𝐵) → 𝑥 ∈ On)
19 rabid 3326 . . . . . . . . 9 (𝑥 ∈ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ↔ (𝑥 ∈ On ∧ 𝐴 ∈ (𝑅1‘suc 𝑥)))
20 intss1 4712 . . . . . . . . 9 (𝑥 ∈ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} → {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥)
2119, 20sylbir 227 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝐴 ∈ (𝑅1‘suc 𝑥)) → {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥)
2218, 21sylan 575 . . . . . . 7 (((𝐵 ∈ dom 𝑅1𝑥𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝑥)) → {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥)
2322ex 403 . . . . . 6 ((𝐵 ∈ dom 𝑅1𝑥𝐵) → (𝐴 ∈ (𝑅1‘suc 𝑥) → {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥))
2415, 23sylbird 252 . . . . 5 ((𝐵 ∈ dom 𝑅1𝑥𝐵) → (𝐴 ∈ 𝒫 (𝑅1𝑥) → {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥))
2524reximdva 3225 . . . 4 (𝐵 ∈ dom 𝑅1 → (∃𝑥𝐵 𝐴 ∈ 𝒫 (𝑅1𝑥) → ∃𝑥𝐵 {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥))
265, 25sylbid 232 . . 3 (𝐵 ∈ dom 𝑅1 → (𝐴 ∈ (𝑅1𝐵) → ∃𝑥𝐵 {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥))
271, 26mpcom 38 . 2 (𝐴 ∈ (𝑅1𝐵) → ∃𝑥𝐵 {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥)
28 r1elwf 8936 . . . . . . 7 (𝐴 ∈ (𝑅1𝐵) → 𝐴 (𝑅1 “ On))
29 rankvalb 8937 . . . . . . 7 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
3028, 29syl 17 . . . . . 6 (𝐴 ∈ (𝑅1𝐵) → (rank‘𝐴) = {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
3130sseq1d 3857 . . . . 5 (𝐴 ∈ (𝑅1𝐵) → ((rank‘𝐴) ⊆ 𝑥 {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥))
3231adantr 474 . . . 4 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝑥𝐵) → ((rank‘𝐴) ⊆ 𝑥 {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥))
33 rankon 8935 . . . . . . 7 (rank‘𝐴) ∈ On
3417, 1sseldi 3825 . . . . . . 7 (𝐴 ∈ (𝑅1𝐵) → 𝐵 ∈ On)
35 ontr2 6010 . . . . . . 7 (((rank‘𝐴) ∈ On ∧ 𝐵 ∈ On) → (((rank‘𝐴) ⊆ 𝑥𝑥𝐵) → (rank‘𝐴) ∈ 𝐵))
3633, 34, 35sylancr 581 . . . . . 6 (𝐴 ∈ (𝑅1𝐵) → (((rank‘𝐴) ⊆ 𝑥𝑥𝐵) → (rank‘𝐴) ∈ 𝐵))
3736expcomd 408 . . . . 5 (𝐴 ∈ (𝑅1𝐵) → (𝑥𝐵 → ((rank‘𝐴) ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵)))
3837imp 397 . . . 4 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝑥𝐵) → ((rank‘𝐴) ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵))
3932, 38sylbird 252 . . 3 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝑥𝐵) → ( {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵))
4039rexlimdva 3240 . 2 (𝐴 ∈ (𝑅1𝐵) → (∃𝑥𝐵 {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵))
4127, 40mpd 15 1 (𝐴 ∈ (𝑅1𝐵) → (rank‘𝐴) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1656  wcel 2164  wrex 3118  {crab 3121  wss 3798  𝒫 cpw 4378   cuni 4658   cint 4697   ciun 4740  dom cdm 5342  cima 5345  Ord word 5962  Oncon0 5963  Lim wlim 5964  suc csuc 5965  Fun wfun 6117  cfv 6123  𝑅1cr1 8902  rankcrnk 8903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-om 7327  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-r1 8904  df-rank 8905
This theorem is referenced by:  rankr1ag  8942  tcrank  9024  dfac12lem1  9280  dfac12lem2  9281  r1limwun  9873  inatsk  9915  aomclem4  38463
  Copyright terms: Public domain W3C validator