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 ) )