Metamath Proof Explorer

Theorem rankr1ai

Description: One direction of rankr1a . (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankr1ai 
|- ( A e. ( R1 ` B ) -> ( rank ` A ) e. B )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( A e. ( R1 ` B ) -> B e. dom R1 )
2 r1val1 
 |-  ( B e. dom R1 -> ( R1 ` B ) = U_ x e. B ~P ( R1 ` x ) )
3 2 eleq2d 
 |-  ( B e. dom R1 -> ( A e. ( R1 ` B ) <-> A e. U_ x e. B ~P ( R1 ` x ) ) )
4 eliun 
 |-  ( A e. U_ x e. B ~P ( R1 ` x ) <-> E. x e. B A e. ~P ( R1 ` x ) )
5 3 4 bitrdi 
 |-  ( B e. dom R1 -> ( A e. ( R1 ` B ) <-> E. x e. B A e. ~P ( R1 ` x ) ) )
6 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
7 6 simpri 
 |-  Lim dom R1
8 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
9 7 8 ax-mp 
 |-  Ord dom R1
10 ordtr1 
 |-  ( Ord dom R1 -> ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 ) )
11 9 10 ax-mp 
 |-  ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 )
12 11 ancoms 
 |-  ( ( B e. dom R1 /\ x e. B ) -> x e. dom R1 )
13 r1sucg 
 |-  ( x e. dom R1 -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
14 13 eleq2d 
 |-  ( x e. dom R1 -> ( A e. ( R1 ` suc x ) <-> A e. ~P ( R1 ` x ) ) )
15 12 14 syl 
 |-  ( ( B e. dom R1 /\ x e. B ) -> ( A e. ( R1 ` suc x ) <-> A e. ~P ( R1 ` x ) ) )
16 ordsson 
 |-  ( Ord dom R1 -> dom R1 C_ On )
17 9 16 ax-mp 
 |-  dom R1 C_ On
18 17 12 sseldi 
 |-  ( ( B e. dom R1 /\ x e. B ) -> x e. On )
19 rabid 
 |-  ( x e. { x e. On | A e. ( R1 ` suc x ) } <-> ( x e. On /\ A e. ( R1 ` suc x ) ) )
20 intss1 
 |-  ( x e. { x e. On | A e. ( R1 ` suc x ) } -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x )
21 19 20 sylbir 
 |-  ( ( x e. On /\ A e. ( R1 ` suc x ) ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x )
22 18 21 sylan 
 |-  ( ( ( B e. dom R1 /\ x e. B ) /\ A e. ( R1 ` suc x ) ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x )
23 22 ex 
 |-  ( ( B e. dom R1 /\ x e. B ) -> ( A e. ( R1 ` suc x ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) )
24 15 23 sylbird 
 |-  ( ( B e. dom R1 /\ x e. B ) -> ( A e. ~P ( R1 ` x ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) )
25 24 reximdva 
 |-  ( B e. dom R1 -> ( E. x e. B A e. ~P ( R1 ` x ) -> E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) )
26 5 25 sylbid 
 |-  ( B e. dom R1 -> ( A e. ( R1 ` B ) -> E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) )
27 1 26 mpcom 
 |-  ( A e. ( R1 ` B ) -> E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x )
28 r1elwf 
 |-  ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )
29 rankvalb 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )
30 28 29 syl 
 |-  ( A e. ( R1 ` B ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )
31 30 sseq1d 
 |-  ( A e. ( R1 ` B ) -> ( ( rank ` A ) C_ x <-> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) )
32 31 adantr 
 |-  ( ( A e. ( R1 ` B ) /\ x e. B ) -> ( ( rank ` A ) C_ x <-> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) )
33 rankon 
 |-  ( rank ` A ) e. On
34 17 1 sseldi 
 |-  ( A e. ( R1 ` B ) -> B e. On )
35 ontr2 
 |-  ( ( ( rank ` A ) e. On /\ B e. On ) -> ( ( ( rank ` A ) C_ x /\ x e. B ) -> ( rank ` A ) e. B ) )
36 33 34 35 sylancr 
 |-  ( A e. ( R1 ` B ) -> ( ( ( rank ` A ) C_ x /\ x e. B ) -> ( rank ` A ) e. B ) )
37 36 expcomd 
 |-  ( A e. ( R1 ` B ) -> ( x e. B -> ( ( rank ` A ) C_ x -> ( rank ` A ) e. B ) ) )
38 37 imp 
 |-  ( ( A e. ( R1 ` B ) /\ x e. B ) -> ( ( rank ` A ) C_ x -> ( rank ` A ) e. B ) )
39 32 38 sylbird 
 |-  ( ( A e. ( R1 ` B ) /\ x e. B ) -> ( |^| { x e. On | A e. ( R1 ` suc x ) } C_ x -> ( rank ` A ) e. B ) )
40 39 rexlimdva 
 |-  ( A e. ( R1 ` B ) -> ( E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x -> ( rank ` A ) e. B ) )
41 27 40 mpd 
 |-  ( A e. ( R1 ` B ) -> ( rank ` A ) e. B )