This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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