Metamath Proof Explorer

Theorem rankonidlem

Description: Lemma for rankonid . (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion rankonidlem 
|- ( A e. dom R1 -> ( A e. U. ( R1 " On ) /\ ( rank ` A ) = A ) )

Proof

Step Hyp Ref Expression
1 r1dmlim 
 |-  Lim dom R1
2 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
3 1 2 ax-mp 
 |-  Ord dom R1
4 ordelon 
 |-  ( ( Ord dom R1 /\ A e. dom R1 ) -> A e. On )
5 3 4 mpan 
 |-  ( A e. dom R1 -> A e. On )
6 eleq1 
 |-  ( x = y -> ( x e. dom R1 <-> y e. dom R1 ) )
7 eleq1 
 |-  ( x = y -> ( x e. U. ( R1 " On ) <-> y e. U. ( R1 " On ) ) )
8 fveq2 
 |-  ( x = y -> ( rank ` x ) = ( rank ` y ) )
9 id 
 |-  ( x = y -> x = y )
10 8 9 eqeq12d 
 |-  ( x = y -> ( ( rank ` x ) = x <-> ( rank ` y ) = y ) )
11 7 10 anbi12d 
 |-  ( x = y -> ( ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) <-> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) )
12 6 11 imbi12d 
 |-  ( x = y -> ( ( x e. dom R1 -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) ) <-> ( y e. dom R1 -> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) ) )
13 eleq1 
 |-  ( x = A -> ( x e. dom R1 <-> A e. dom R1 ) )
14 eleq1 
 |-  ( x = A -> ( x e. U. ( R1 " On ) <-> A e. U. ( R1 " On ) ) )
15 fveq2 
 |-  ( x = A -> ( rank ` x ) = ( rank ` A ) )
16 id 
 |-  ( x = A -> x = A )
17 15 16 eqeq12d 
 |-  ( x = A -> ( ( rank ` x ) = x <-> ( rank ` A ) = A ) )
18 14 17 anbi12d 
 |-  ( x = A -> ( ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) <-> ( A e. U. ( R1 " On ) /\ ( rank ` A ) = A ) ) )
19 13 18 imbi12d 
 |-  ( x = A -> ( ( x e. dom R1 -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) ) <-> ( A e. dom R1 -> ( A e. U. ( R1 " On ) /\ ( rank ` A ) = A ) ) ) )
20 ordtr1 
 |-  ( Ord dom R1 -> ( ( y e. x /\ x e. dom R1 ) -> y e. dom R1 ) )
21 3 20 ax-mp 
 |-  ( ( y e. x /\ x e. dom R1 ) -> y e. dom R1 )
22 21 ancoms 
 |-  ( ( x e. dom R1 /\ y e. x ) -> y e. dom R1 )
23 pm5.5 
 |-  ( y e. dom R1 -> ( ( y e. dom R1 -> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) <-> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) )
24 22 23 syl 
 |-  ( ( x e. dom R1 /\ y e. x ) -> ( ( y e. dom R1 -> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) <-> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) )
25 24 ralbidva 
 |-  ( x e. dom R1 -> ( A. y e. x ( y e. dom R1 -> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) <-> A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) )
26 simplr 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> y e. x )
27 ordelon 
 |-  ( ( Ord dom R1 /\ x e. dom R1 ) -> x e. On )
28 3 27 mpan 
 |-  ( x e. dom R1 -> x e. On )
29 28 ad2antrr 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> x e. On )
30 eloni 
 |-  ( x e. On -> Ord x )
31 29 30 syl 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> Ord x )
32 ordelsuc 
 |-  ( ( y e. x /\ Ord x ) -> ( y e. x <-> suc y C_ x ) )
33 26 31 32 syl2anc 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( y e. x <-> suc y C_ x ) )
34 26 33 mpbid 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> suc y C_ x )
35 22 adantr 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> y e. dom R1 )
36 limsuc 
 |-  ( Lim dom R1 -> ( y e. dom R1 <-> suc y e. dom R1 ) )
37 1 36 ax-mp 
 |-  ( y e. dom R1 <-> suc y e. dom R1 )
38 35 37 sylib 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> suc y e. dom R1 )
39 simpll 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> x e. dom R1 )
40 r1ord3g 
 |-  ( ( suc y e. dom R1 /\ x e. dom R1 ) -> ( suc y C_ x -> ( R1 ` suc y ) C_ ( R1 ` x ) ) )
41 38 39 40 syl2anc 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( suc y C_ x -> ( R1 ` suc y ) C_ ( R1 ` x ) ) )
42 34 41 mpd 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( R1 ` suc y ) C_ ( R1 ` x ) )
43 rankidb 
 |-  ( y e. U. ( R1 " On ) -> y e. ( R1 ` suc ( rank ` y ) ) )
44 43 ad2antrl 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> y e. ( R1 ` suc ( rank ` y ) ) )
45 suceq 
 |-  ( ( rank ` y ) = y -> suc ( rank ` y ) = suc y )
46 45 ad2antll 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> suc ( rank ` y ) = suc y )
47 46 fveq2d 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( R1 ` suc ( rank ` y ) ) = ( R1 ` suc y ) )
48 44 47 eleqtrd 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> y e. ( R1 ` suc y ) )
49 42 48 sseldd 
 |-  ( ( ( x e. dom R1 /\ y e. x ) /\ ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> y e. ( R1 ` x ) )
50 49 ex 
 |-  ( ( x e. dom R1 /\ y e. x ) -> ( ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> y e. ( R1 ` x ) ) )
51 50 ralimdva 
 |-  ( x e. dom R1 -> ( A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> A. y e. x y e. ( R1 ` x ) ) )
52 51 imp 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> A. y e. x y e. ( R1 ` x ) )
53 dfss3 
 |-  ( x C_ ( R1 ` x ) <-> A. y e. x y e. ( R1 ` x ) )
54 52 53 sylibr 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> x C_ ( R1 ` x ) )
55 vex 
 |-  x e. _V
56 55 elpw 
 |-  ( x e. ~P ( R1 ` x ) <-> x C_ ( R1 ` x ) )
57 54 56 sylibr 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> x e. ~P ( R1 ` x ) )
58 r1sucg 
 |-  ( x e. dom R1 -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
59 58 adantr 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
60 57 59 eleqtrrd 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> x e. ( R1 ` suc x ) )
61 r1elwf 
 |-  ( x e. ( R1 ` suc x ) -> x e. U. ( R1 " On ) )
62 60 61 syl 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> x e. U. ( R1 " On ) )
63 rankval3b 
 |-  ( x e. U. ( R1 " On ) -> ( rank ` x ) = |^| { z e. On | A. y e. x ( rank ` y ) e. z } )
64 62 63 syl 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( rank ` x ) = |^| { z e. On | A. y e. x ( rank ` y ) e. z } )
65 eleq1 
 |-  ( ( rank ` y ) = y -> ( ( rank ` y ) e. z <-> y e. z ) )
66 65 adantl 
 |-  ( ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> ( ( rank ` y ) e. z <-> y e. z ) )
67 66 ralimi 
 |-  ( A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> A. y e. x ( ( rank ` y ) e. z <-> y e. z ) )
68 ralbi 
 |-  ( A. y e. x ( ( rank ` y ) e. z <-> y e. z ) -> ( A. y e. x ( rank ` y ) e. z <-> A. y e. x y e. z ) )
69 67 68 syl 
 |-  ( A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> ( A. y e. x ( rank ` y ) e. z <-> A. y e. x y e. z ) )
70 dfss3 
 |-  ( x C_ z <-> A. y e. x y e. z )
71 69 70 bitr4di 
 |-  ( A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> ( A. y e. x ( rank ` y ) e. z <-> x C_ z ) )
72 71 rabbidv 
 |-  ( A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> { z e. On | A. y e. x ( rank ` y ) e. z } = { z e. On | x C_ z } )
73 72 inteqd 
 |-  ( A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> |^| { z e. On | A. y e. x ( rank ` y ) e. z } = |^| { z e. On | x C_ z } )
74 73 adantl 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> |^| { z e. On | A. y e. x ( rank ` y ) e. z } = |^| { z e. On | x C_ z } )
75 28 adantr 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> x e. On )
76 intmin 
 |-  ( x e. On -> |^| { z e. On | x C_ z } = x )
77 75 76 syl 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> |^| { z e. On | x C_ z } = x )
78 64 74 77 3eqtrd 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( rank ` x ) = x )
79 62 78 jca 
 |-  ( ( x e. dom R1 /\ A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) )
80 79 ex 
 |-  ( x e. dom R1 -> ( A. y e. x ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) ) )
81 25 80 sylbid 
 |-  ( x e. dom R1 -> ( A. y e. x ( y e. dom R1 -> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) ) )
82 81 com12 
 |-  ( A. y e. x ( y e. dom R1 -> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( x e. dom R1 -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) ) )
83 82 a1i 
 |-  ( x e. On -> ( A. y e. x ( y e. dom R1 -> ( y e. U. ( R1 " On ) /\ ( rank ` y ) = y ) ) -> ( x e. dom R1 -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) ) ) )
84 12 19 83 tfis3 
 |-  ( A e. On -> ( A e. dom R1 -> ( A e. U. ( R1 " On ) /\ ( rank ` A ) = A ) ) )
85 5 84 mpcom 
 |-  ( A e. dom R1 -> ( A e. U. ( R1 " On ) /\ ( rank ` A ) = A ) )