Metamath Proof Explorer

Theorem ttukeylem5

Description: Lemma for ttukey . The G function forms a (transfinitely long) chain of inclusions. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1 
|- ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
ttukeylem.2 
|- ( ph -> B e. A )
ttukeylem.3 
|- ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
ttukeylem.4 
|- G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) )
Assertion ttukeylem5 
|- ( ( ph /\ ( C e. On /\ D e. On /\ C C_ D ) ) -> ( G ` C ) C_ ( G ` D ) )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 
 |-  ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
2 ttukeylem.2 
 |-  ( ph -> B e. A )
3 ttukeylem.3 
 |-  ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
4 ttukeylem.4 
 |-  G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) )
5 sseq2 
 |-  ( y = a -> ( C C_ y <-> C C_ a ) )
6 fveq2 
 |-  ( y = a -> ( G ` y ) = ( G ` a ) )
7 6 sseq2d 
 |-  ( y = a -> ( ( G ` C ) C_ ( G ` y ) <-> ( G ` C ) C_ ( G ` a ) ) )
8 5 7 imbi12d 
 |-  ( y = a -> ( ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) <-> ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) )
9 8 imbi2d 
 |-  ( y = a -> ( ( ( ph /\ C e. On ) -> ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) ) <-> ( ( ph /\ C e. On ) -> ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) ) )
10 sseq2 
 |-  ( y = D -> ( C C_ y <-> C C_ D ) )
11 fveq2 
 |-  ( y = D -> ( G ` y ) = ( G ` D ) )
12 11 sseq2d 
 |-  ( y = D -> ( ( G ` C ) C_ ( G ` y ) <-> ( G ` C ) C_ ( G ` D ) ) )
13 10 12 imbi12d 
 |-  ( y = D -> ( ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) <-> ( C C_ D -> ( G ` C ) C_ ( G ` D ) ) ) )
14 13 imbi2d 
 |-  ( y = D -> ( ( ( ph /\ C e. On ) -> ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) ) <-> ( ( ph /\ C e. On ) -> ( C C_ D -> ( G ` C ) C_ ( G ` D ) ) ) ) )
15 r19.21v 
 |-  ( A. a e. y ( ( ph /\ C e. On ) -> ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) <-> ( ( ph /\ C e. On ) -> A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) )
16 onsseleq 
 |-  ( ( C e. On /\ y e. On ) -> ( C C_ y <-> ( C e. y \/ C = y ) ) )
17 16 ad4ant23 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) -> ( C C_ y <-> ( C e. y \/ C = y ) ) )
18 sseq2 
 |-  ( if ( y = (/) , B , U. ( G " y ) ) = if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) -> ( ( G ` C ) C_ if ( y = (/) , B , U. ( G " y ) ) <-> ( G ` C ) C_ if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) ) )
19 sseq2 
 |-  ( ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) = if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) -> ( ( G ` C ) C_ ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) <-> ( G ` C ) C_ if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) ) )
20 4 tfr1 
 |-  G Fn On
21 simplr 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> y e. On )
22 onss 
 |-  ( y e. On -> y C_ On )
23 21 22 syl 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> y C_ On )
24 simprr 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> C e. y )
25 fnfvima 
 |-  ( ( G Fn On /\ y C_ On /\ C e. y ) -> ( G ` C ) e. ( G " y ) )
26 20 23 24 25 mp3an2i 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> ( G ` C ) e. ( G " y ) )
27 elssuni 
 |-  ( ( G ` C ) e. ( G " y ) -> ( G ` C ) C_ U. ( G " y ) )
28 26 27 syl 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> ( G ` C ) C_ U. ( G " y ) )
29 n0i 
 |-  ( C e. y -> -. y = (/) )
30 iffalse 
 |-  ( -. y = (/) -> if ( y = (/) , B , U. ( G " y ) ) = U. ( G " y ) )
31 24 29 30 3syl 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> if ( y = (/) , B , U. ( G " y ) ) = U. ( G " y ) )
32 28 31 sseqtrrd 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> ( G ` C ) C_ if ( y = (/) , B , U. ( G " y ) ) )
33 32 adantr 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ y = U. y ) -> ( G ` C ) C_ if ( y = (/) , B , U. ( G " y ) ) )
34 24 adantr 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> C e. y )
35 elssuni 
 |-  ( C e. y -> C C_ U. y )
36 34 35 syl 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> C C_ U. y )
37 sseq2 
 |-  ( a = U. y -> ( C C_ a <-> C C_ U. y ) )
38 fveq2 
 |-  ( a = U. y -> ( G ` a ) = ( G ` U. y ) )
39 38 sseq2d 
 |-  ( a = U. y -> ( ( G ` C ) C_ ( G ` a ) <-> ( G ` C ) C_ ( G ` U. y ) ) )
40 37 39 imbi12d 
 |-  ( a = U. y -> ( ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) <-> ( C C_ U. y -> ( G ` C ) C_ ( G ` U. y ) ) ) )
41 simplrl 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) )
42 vuniex 
 |-  U. y e. _V
43 42 sucid 
 |-  U. y e. suc U. y
44 eloni 
 |-  ( y e. On -> Ord y )
45 orduniorsuc 
 |-  ( Ord y -> ( y = U. y \/ y = suc U. y ) )
46 21 44 45 3syl 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> ( y = U. y \/ y = suc U. y ) )
47 46 orcanai 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> y = suc U. y )
48 43 47 eleqtrrid 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> U. y e. y )
49 40 41 48 rspcdva 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> ( C C_ U. y -> ( G ` C ) C_ ( G ` U. y ) ) )
50 36 49 mpd 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> ( G ` C ) C_ ( G ` U. y ) )
51 ssun1 
 |-  ( G ` U. y ) C_ ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) )
52 50 51 sstrdi 
 |-  ( ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) /\ -. y = U. y ) -> ( G ` C ) C_ ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) )
53 18 19 33 52 ifbothda 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> ( G ` C ) C_ if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) )
54 1 2 3 4 ttukeylem3 
 |-  ( ( ph /\ y e. On ) -> ( G ` y ) = if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) )
55 54 ad4ant13 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> ( G ` y ) = if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) )
56 53 55 sseqtrrd 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) /\ C e. y ) ) -> ( G ` C ) C_ ( G ` y ) )
57 56 expr 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) -> ( C e. y -> ( G ` C ) C_ ( G ` y ) ) )
58 fveq2 
 |-  ( C = y -> ( G ` C ) = ( G ` y ) )
59 eqimss 
 |-  ( ( G ` C ) = ( G ` y ) -> ( G ` C ) C_ ( G ` y ) )
60 58 59 syl 
 |-  ( C = y -> ( G ` C ) C_ ( G ` y ) )
61 60 a1i 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) -> ( C = y -> ( G ` C ) C_ ( G ` y ) ) )
62 57 61 jaod 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) -> ( ( C e. y \/ C = y ) -> ( G ` C ) C_ ( G ` y ) ) )
63 17 62 sylbid 
 |-  ( ( ( ( ph /\ C e. On ) /\ y e. On ) /\ A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) -> ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) )
64 63 ex 
 |-  ( ( ( ph /\ C e. On ) /\ y e. On ) -> ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) -> ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) ) )
65 64 expcom 
 |-  ( y e. On -> ( ( ph /\ C e. On ) -> ( A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) -> ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) ) ) )
66 65 a2d 
 |-  ( y e. On -> ( ( ( ph /\ C e. On ) -> A. a e. y ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) -> ( ( ph /\ C e. On ) -> ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) ) ) )
67 15 66 biimtrid 
 |-  ( y e. On -> ( A. a e. y ( ( ph /\ C e. On ) -> ( C C_ a -> ( G ` C ) C_ ( G ` a ) ) ) -> ( ( ph /\ C e. On ) -> ( C C_ y -> ( G ` C ) C_ ( G ` y ) ) ) ) )
68 9 14 67 tfis3 
 |-  ( D e. On -> ( ( ph /\ C e. On ) -> ( C C_ D -> ( G ` C ) C_ ( G ` D ) ) ) )
69 68 expdcom 
 |-  ( ph -> ( C e. On -> ( D e. On -> ( C C_ D -> ( G ` C ) C_ ( G ` D ) ) ) ) )
70 69 3imp2 
 |-  ( ( ph /\ ( C e. On /\ D e. On /\ C C_ D ) ) -> ( G ` C ) C_ ( G ` D ) )