Metamath Proof Explorer

Theorem cfsmolem

Description: Lemma for cfsmo . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Hypotheses cfsmolem.2 
|- F = ( z e. _V |-> ( ( g ` dom z ) u. U_ t e. dom z suc ( z ` t ) ) )
cfsmolem.3 
|- G = ( recs ( F ) |` ( cf ` A ) )
Assertion cfsmolem 
|- ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )

Proof

Step Hyp Ref Expression
1 cfsmolem.2 
 |-  F = ( z e. _V |-> ( ( g ` dom z ) u. U_ t e. dom z suc ( z ` t ) ) )
2 cfsmolem.3 
 |-  G = ( recs ( F ) |` ( cf ` A ) )
3 cff1 
 |-  ( A e. On -> E. g ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) )
4 cfon 
 |-  ( cf ` A ) e. On
5 4 oneli 
 |-  ( x e. ( cf ` A ) -> x e. On )
6 5 3ad2ant3 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> x e. On )
7 eleq1w 
 |-  ( x = y -> ( x e. ( cf ` A ) <-> y e. ( cf ` A ) ) )
8 7 3anbi3d 
 |-  ( x = y -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) <-> ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) ) )
9 fveq2 
 |-  ( x = y -> ( G ` x ) = ( G ` y ) )
10 9 eleq1d 
 |-  ( x = y -> ( ( G ` x ) e. A <-> ( G ` y ) e. A ) )
11 8 10 imbi12d 
 |-  ( x = y -> ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) <-> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) ) )
12 simpl1 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> g : ( cf ` A ) -1-1-> A )
13 simpl2 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> A e. On )
14 ontr1 
 |-  ( ( cf ` A ) e. On -> ( ( y e. x /\ x e. ( cf ` A ) ) -> y e. ( cf ` A ) ) )
15 4 14 ax-mp 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> y e. ( cf ` A ) )
16 15 ancoms 
 |-  ( ( x e. ( cf ` A ) /\ y e. x ) -> y e. ( cf ` A ) )
17 16 3ad2antl3 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> y e. ( cf ` A ) )
18 pm2.27 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( G ` y ) e. A ) )
19 12 13 17 18 syl3anc 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( G ` y ) e. A ) )
20 19 ralimdva 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> A. y e. x ( G ` y ) e. A ) )
21 2 fveq1i 
 |-  ( G ` x ) = ( ( recs ( F ) |` ( cf ` A ) ) ` x )
22 fvres 
 |-  ( x e. ( cf ` A ) -> ( ( recs ( F ) |` ( cf ` A ) ) ` x ) = ( recs ( F ) ` x ) )
23 21 22 eqtrid 
 |-  ( x e. ( cf ` A ) -> ( G ` x ) = ( recs ( F ) ` x ) )
24 recsval 
 |-  ( x e. On -> ( recs ( F ) ` x ) = ( F ` ( recs ( F ) |` x ) ) )
25 recsfnon 
 |-  recs ( F ) Fn On
26 fnfun 
 |-  ( recs ( F ) Fn On -> Fun recs ( F ) )
27 25 26 ax-mp 
 |-  Fun recs ( F )
28 vex 
 |-  x e. _V
29 resfunexg 
 |-  ( ( Fun recs ( F ) /\ x e. _V ) -> ( recs ( F ) |` x ) e. _V )
30 27 28 29 mp2an 
 |-  ( recs ( F ) |` x ) e. _V
31 dmeq 
 |-  ( z = ( recs ( F ) |` x ) -> dom z = dom ( recs ( F ) |` x ) )
32 31 fveq2d 
 |-  ( z = ( recs ( F ) |` x ) -> ( g ` dom z ) = ( g ` dom ( recs ( F ) |` x ) ) )
33 fveq1 
 |-  ( z = ( recs ( F ) |` x ) -> ( z ` t ) = ( ( recs ( F ) |` x ) ` t ) )
34 suceq 
 |-  ( ( z ` t ) = ( ( recs ( F ) |` x ) ` t ) -> suc ( z ` t ) = suc ( ( recs ( F ) |` x ) ` t ) )
35 33 34 syl 
 |-  ( z = ( recs ( F ) |` x ) -> suc ( z ` t ) = suc ( ( recs ( F ) |` x ) ` t ) )
36 31 35 iuneq12d 
 |-  ( z = ( recs ( F ) |` x ) -> U_ t e. dom z suc ( z ` t ) = U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) )
37 32 36 uneq12d 
 |-  ( z = ( recs ( F ) |` x ) -> ( ( g ` dom z ) u. U_ t e. dom z suc ( z ` t ) ) = ( ( g ` dom ( recs ( F ) |` x ) ) u. U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) ) )
38 fvex 
 |-  ( g ` dom ( recs ( F ) |` x ) ) e. _V
39 30 dmex 
 |-  dom ( recs ( F ) |` x ) e. _V
40 fvex 
 |-  ( ( recs ( F ) |` x ) ` t ) e. _V
41 40 sucex 
 |-  suc ( ( recs ( F ) |` x ) ` t ) e. _V
42 39 41 iunex 
 |-  U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) e. _V
43 38 42 unex 
 |-  ( ( g ` dom ( recs ( F ) |` x ) ) u. U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) ) e. _V
44 37 1 43 fvmpt 
 |-  ( ( recs ( F ) |` x ) e. _V -> ( F ` ( recs ( F ) |` x ) ) = ( ( g ` dom ( recs ( F ) |` x ) ) u. U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) ) )
45 30 44 ax-mp 
 |-  ( F ` ( recs ( F ) |` x ) ) = ( ( g ` dom ( recs ( F ) |` x ) ) u. U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) )
46 24 45 eqtrdi 
 |-  ( x e. On -> ( recs ( F ) ` x ) = ( ( g ` dom ( recs ( F ) |` x ) ) u. U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) ) )
47 onss 
 |-  ( x e. On -> x C_ On )
48 fnssres 
 |-  ( ( recs ( F ) Fn On /\ x C_ On ) -> ( recs ( F ) |` x ) Fn x )
49 25 47 48 sylancr 
 |-  ( x e. On -> ( recs ( F ) |` x ) Fn x )
50 fndm 
 |-  ( ( recs ( F ) |` x ) Fn x -> dom ( recs ( F ) |` x ) = x )
51 fveq2 
 |-  ( dom ( recs ( F ) |` x ) = x -> ( g ` dom ( recs ( F ) |` x ) ) = ( g ` x ) )
52 iuneq1 
 |-  ( dom ( recs ( F ) |` x ) = x -> U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) = U_ t e. x suc ( ( recs ( F ) |` x ) ` t ) )
53 fvres 
 |-  ( t e. x -> ( ( recs ( F ) |` x ) ` t ) = ( recs ( F ) ` t ) )
54 suceq 
 |-  ( ( ( recs ( F ) |` x ) ` t ) = ( recs ( F ) ` t ) -> suc ( ( recs ( F ) |` x ) ` t ) = suc ( recs ( F ) ` t ) )
55 53 54 syl 
 |-  ( t e. x -> suc ( ( recs ( F ) |` x ) ` t ) = suc ( recs ( F ) ` t ) )
56 55 iuneq2i 
 |-  U_ t e. x suc ( ( recs ( F ) |` x ) ` t ) = U_ t e. x suc ( recs ( F ) ` t )
57 fveq2 
 |-  ( y = t -> ( recs ( F ) ` y ) = ( recs ( F ) ` t ) )
58 suceq 
 |-  ( ( recs ( F ) ` y ) = ( recs ( F ) ` t ) -> suc ( recs ( F ) ` y ) = suc ( recs ( F ) ` t ) )
59 57 58 syl 
 |-  ( y = t -> suc ( recs ( F ) ` y ) = suc ( recs ( F ) ` t ) )
60 59 cbviunv 
 |-  U_ y e. x suc ( recs ( F ) ` y ) = U_ t e. x suc ( recs ( F ) ` t )
61 56 60 eqtr4i 
 |-  U_ t e. x suc ( ( recs ( F ) |` x ) ` t ) = U_ y e. x suc ( recs ( F ) ` y )
62 52 61 eqtrdi 
 |-  ( dom ( recs ( F ) |` x ) = x -> U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) = U_ y e. x suc ( recs ( F ) ` y ) )
63 51 62 uneq12d 
 |-  ( dom ( recs ( F ) |` x ) = x -> ( ( g ` dom ( recs ( F ) |` x ) ) u. U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) ) = ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
64 49 50 63 3syl 
 |-  ( x e. On -> ( ( g ` dom ( recs ( F ) |` x ) ) u. U_ t e. dom ( recs ( F ) |` x ) suc ( ( recs ( F ) |` x ) ` t ) ) = ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
65 46 64 eqtrd 
 |-  ( x e. On -> ( recs ( F ) ` x ) = ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
66 5 65 syl 
 |-  ( x e. ( cf ` A ) -> ( recs ( F ) ` x ) = ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
67 23 66 eqtrd 
 |-  ( x e. ( cf ` A ) -> ( G ` x ) = ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
68 67 3ad2ant2 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( G ` x ) = ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
69 eloni 
 |-  ( A e. On -> Ord A )
70 69 adantl 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> Ord A )
71 70 3ad2ant1 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> Ord A )
72 f1f 
 |-  ( g : ( cf ` A ) -1-1-> A -> g : ( cf ` A ) --> A )
73 72 ffvelrnda 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ x e. ( cf ` A ) ) -> ( g ` x ) e. A )
74 73 adantlr 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) ) -> ( g ` x ) e. A )
75 74 3adant3 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( g ` x ) e. A )
76 2 fveq1i 
 |-  ( G ` y ) = ( ( recs ( F ) |` ( cf ` A ) ) ` y )
77 15 fvresd 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> ( ( recs ( F ) |` ( cf ` A ) ) ` y ) = ( recs ( F ) ` y ) )
78 76 77 eqtrid 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> ( G ` y ) = ( recs ( F ) ` y ) )
79 78 adantrl 
 |-  ( ( y e. x /\ ( A e. On /\ x e. ( cf ` A ) ) ) -> ( G ` y ) = ( recs ( F ) ` y ) )
80 79 ancoms 
 |-  ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( G ` y ) = ( recs ( F ) ` y ) )
81 80 eleq1d 
 |-  ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A <-> ( recs ( F ) ` y ) e. A ) )
82 ordsucss 
 |-  ( Ord A -> ( ( recs ( F ) ` y ) e. A -> suc ( recs ( F ) ` y ) C_ A ) )
83 69 82 syl 
 |-  ( A e. On -> ( ( recs ( F ) ` y ) e. A -> suc ( recs ( F ) ` y ) C_ A ) )
84 83 ad2antrr 
 |-  ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( recs ( F ) ` y ) e. A -> suc ( recs ( F ) ` y ) C_ A ) )
85 81 84 sylbid 
 |-  ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A -> suc ( recs ( F ) ` y ) C_ A ) )
86 85 ralimdva 
 |-  ( ( A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> A. y e. x suc ( recs ( F ) ` y ) C_ A ) )
87 iunss 
 |-  ( U_ y e. x suc ( recs ( F ) ` y ) C_ A <-> A. y e. x suc ( recs ( F ) ` y ) C_ A )
88 86 87 syl6ibr 
 |-  ( ( A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> U_ y e. x suc ( recs ( F ) ` y ) C_ A ) )
89 88 3impia 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc ( recs ( F ) ` y ) C_ A )
90 onelon 
 |-  ( ( A e. On /\ ( recs ( F ) ` y ) e. A ) -> ( recs ( F ) ` y ) e. On )
91 90 ex 
 |-  ( A e. On -> ( ( recs ( F ) ` y ) e. A -> ( recs ( F ) ` y ) e. On ) )
92 91 ad2antrr 
 |-  ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( recs ( F ) ` y ) e. A -> ( recs ( F ) ` y ) e. On ) )
93 81 92 sylbid 
 |-  ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A -> ( recs ( F ) ` y ) e. On ) )
94 suceloni 
 |-  ( ( recs ( F ) ` y ) e. On -> suc ( recs ( F ) ` y ) e. On )
95 93 94 syl6 
 |-  ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A -> suc ( recs ( F ) ` y ) e. On ) )
96 95 ralimdva 
 |-  ( ( A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> A. y e. x suc ( recs ( F ) ` y ) e. On ) )
97 96 3impia 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> A. y e. x suc ( recs ( F ) ` y ) e. On )
98 iunon 
 |-  ( ( x e. _V /\ A. y e. x suc ( recs ( F ) ` y ) e. On ) -> U_ y e. x suc ( recs ( F ) ` y ) e. On )
99 28 97 98 sylancr 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc ( recs ( F ) ` y ) e. On )
100 simp1 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> A e. On )
101 onsseleq 
 |-  ( ( U_ y e. x suc ( recs ( F ) ` y ) e. On /\ A e. On ) -> ( U_ y e. x suc ( recs ( F ) ` y ) C_ A <-> ( U_ y e. x suc ( recs ( F ) ` y ) e. A \/ U_ y e. x suc ( recs ( F ) ` y ) = A ) ) )
102 99 100 101 syl2anc 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc ( recs ( F ) ` y ) C_ A <-> ( U_ y e. x suc ( recs ( F ) ` y ) e. A \/ U_ y e. x suc ( recs ( F ) ` y ) = A ) ) )
103 idd 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc ( recs ( F ) ` y ) e. A -> U_ y e. x suc ( recs ( F ) ` y ) e. A ) )
104 simpll 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> x e. ( cf ` A ) )
105 simprr 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> A e. On )
106 5 ad2antrr 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> x e. On )
107 5 49 syl 
 |-  ( x e. ( cf ` A ) -> ( recs ( F ) |` x ) Fn x )
108 107 adantr 
 |-  ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( recs ( F ) |` x ) Fn x )
109 78 ancoms 
 |-  ( ( x e. ( cf ` A ) /\ y e. x ) -> ( G ` y ) = ( recs ( F ) ` y ) )
110 fvres 
 |-  ( y e. x -> ( ( recs ( F ) |` x ) ` y ) = ( recs ( F ) ` y ) )
111 110 adantl 
 |-  ( ( x e. ( cf ` A ) /\ y e. x ) -> ( ( recs ( F ) |` x ) ` y ) = ( recs ( F ) ` y ) )
112 109 111 eqtr4d 
 |-  ( ( x e. ( cf ` A ) /\ y e. x ) -> ( G ` y ) = ( ( recs ( F ) |` x ) ` y ) )
113 112 eleq1d 
 |-  ( ( x e. ( cf ` A ) /\ y e. x ) -> ( ( G ` y ) e. A <-> ( ( recs ( F ) |` x ) ` y ) e. A ) )
114 113 ralbidva 
 |-  ( x e. ( cf ` A ) -> ( A. y e. x ( G ` y ) e. A <-> A. y e. x ( ( recs ( F ) |` x ) ` y ) e. A ) )
115 114 biimpa 
 |-  ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> A. y e. x ( ( recs ( F ) |` x ) ` y ) e. A )
116 ffnfv 
 |-  ( ( recs ( F ) |` x ) : x --> A <-> ( ( recs ( F ) |` x ) Fn x /\ A. y e. x ( ( recs ( F ) |` x ) ` y ) e. A ) )
117 108 115 116 sylanbrc 
 |-  ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( recs ( F ) |` x ) : x --> A )
118 eleq2 
 |-  ( U_ y e. x suc ( recs ( F ) ` y ) = A -> ( t e. U_ y e. x suc ( recs ( F ) ` y ) <-> t e. A ) )
119 118 biimpar 
 |-  ( ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ t e. A ) -> t e. U_ y e. x suc ( recs ( F ) ` y ) )
120 119 adantrl 
 |-  ( ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> t e. U_ y e. x suc ( recs ( F ) ` y ) )
121 120 3adant1 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ U_ y e. x suc ( recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> t e. U_ y e. x suc ( recs ( F ) ` y ) )
122 onelon 
 |-  ( ( A e. On /\ t e. A ) -> t e. On )
123 110 adantl 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ y e. x ) -> ( ( recs ( F ) |` x ) ` y ) = ( recs ( F ) ` y ) )
124 ffvelrn 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ y e. x ) -> ( ( recs ( F ) |` x ) ` y ) e. A )
125 123 124 eqeltrrd 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ y e. x ) -> ( recs ( F ) ` y ) e. A )
126 125 90 sylan2 
 |-  ( ( A e. On /\ ( ( recs ( F ) |` x ) : x --> A /\ y e. x ) ) -> ( recs ( F ) ` y ) e. On )
127 126 adantlr 
 |-  ( ( ( A e. On /\ t e. A ) /\ ( ( recs ( F ) |` x ) : x --> A /\ y e. x ) ) -> ( recs ( F ) ` y ) e. On )
128 onsssuc 
 |-  ( ( t e. On /\ ( recs ( F ) ` y ) e. On ) -> ( t C_ ( recs ( F ) ` y ) <-> t e. suc ( recs ( F ) ` y ) ) )
129 122 127 128 syl2an2r 
 |-  ( ( ( A e. On /\ t e. A ) /\ ( ( recs ( F ) |` x ) : x --> A /\ y e. x ) ) -> ( t C_ ( recs ( F ) ` y ) <-> t e. suc ( recs ( F ) ` y ) ) )
130 129 anassrs 
 |-  ( ( ( ( A e. On /\ t e. A ) /\ ( recs ( F ) |` x ) : x --> A ) /\ y e. x ) -> ( t C_ ( recs ( F ) ` y ) <-> t e. suc ( recs ( F ) ` y ) ) )
131 130 rexbidva 
 |-  ( ( ( A e. On /\ t e. A ) /\ ( recs ( F ) |` x ) : x --> A ) -> ( E. y e. x t C_ ( recs ( F ) ` y ) <-> E. y e. x t e. suc ( recs ( F ) ` y ) ) )
132 eliun 
 |-  ( t e. U_ y e. x suc ( recs ( F ) ` y ) <-> E. y e. x t e. suc ( recs ( F ) ` y ) )
133 131 132 bitr4di 
 |-  ( ( ( A e. On /\ t e. A ) /\ ( recs ( F ) |` x ) : x --> A ) -> ( E. y e. x t C_ ( recs ( F ) ` y ) <-> t e. U_ y e. x suc ( recs ( F ) ` y ) ) )
134 133 ancoms 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ ( A e. On /\ t e. A ) ) -> ( E. y e. x t C_ ( recs ( F ) ` y ) <-> t e. U_ y e. x suc ( recs ( F ) ` y ) ) )
135 134 3adant2 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ U_ y e. x suc ( recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> ( E. y e. x t C_ ( recs ( F ) ` y ) <-> t e. U_ y e. x suc ( recs ( F ) ` y ) ) )
136 121 135 mpbird 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ U_ y e. x suc ( recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> E. y e. x t C_ ( recs ( F ) ` y ) )
137 136 3expa 
 |-  ( ( ( ( recs ( F ) |` x ) : x --> A /\ U_ y e. x suc ( recs ( F ) ` y ) = A ) /\ ( A e. On /\ t e. A ) ) -> E. y e. x t C_ ( recs ( F ) ` y ) )
138 137 anassrs 
 |-  ( ( ( ( ( recs ( F ) |` x ) : x --> A /\ U_ y e. x suc ( recs ( F ) ` y ) = A ) /\ A e. On ) /\ t e. A ) -> E. y e. x t C_ ( recs ( F ) ` y ) )
139 138 ralrimiva 
 |-  ( ( ( ( recs ( F ) |` x ) : x --> A /\ U_ y e. x suc ( recs ( F ) ` y ) = A ) /\ A e. On ) -> A. t e. A E. y e. x t C_ ( recs ( F ) ` y ) )
140 139 expl 
 |-  ( ( recs ( F ) |` x ) : x --> A -> ( ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) -> A. t e. A E. y e. x t C_ ( recs ( F ) ` y ) ) )
141 117 140 syl 
 |-  ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) -> A. t e. A E. y e. x t C_ ( recs ( F ) ` y ) ) )
142 141 imp 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> A. t e. A E. y e. x t C_ ( recs ( F ) ` y ) )
143 feq1 
 |-  ( f = ( recs ( F ) |` x ) -> ( f : x --> A <-> ( recs ( F ) |` x ) : x --> A ) )
144 fveq1 
 |-  ( f = ( recs ( F ) |` x ) -> ( f ` y ) = ( ( recs ( F ) |` x ) ` y ) )
145 144 sseq2d 
 |-  ( f = ( recs ( F ) |` x ) -> ( t C_ ( f ` y ) <-> t C_ ( ( recs ( F ) |` x ) ` y ) ) )
146 145 rexbidv 
 |-  ( f = ( recs ( F ) |` x ) -> ( E. y e. x t C_ ( f ` y ) <-> E. y e. x t C_ ( ( recs ( F ) |` x ) ` y ) ) )
147 110 sseq2d 
 |-  ( y e. x -> ( t C_ ( ( recs ( F ) |` x ) ` y ) <-> t C_ ( recs ( F ) ` y ) ) )
148 147 rexbiia 
 |-  ( E. y e. x t C_ ( ( recs ( F ) |` x ) ` y ) <-> E. y e. x t C_ ( recs ( F ) ` y ) )
149 146 148 bitrdi 
 |-  ( f = ( recs ( F ) |` x ) -> ( E. y e. x t C_ ( f ` y ) <-> E. y e. x t C_ ( recs ( F ) ` y ) ) )
150 149 ralbidv 
 |-  ( f = ( recs ( F ) |` x ) -> ( A. t e. A E. y e. x t C_ ( f ` y ) <-> A. t e. A E. y e. x t C_ ( recs ( F ) ` y ) ) )
151 143 150 anbi12d 
 |-  ( f = ( recs ( F ) |` x ) -> ( ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) <-> ( ( recs ( F ) |` x ) : x --> A /\ A. t e. A E. y e. x t C_ ( recs ( F ) ` y ) ) ) )
152 30 151 spcev 
 |-  ( ( ( recs ( F ) |` x ) : x --> A /\ A. t e. A E. y e. x t C_ ( recs ( F ) ` y ) ) -> E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) )
153 117 142 152 syl2an2r 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) )
154 cfflb 
 |-  ( ( A e. On /\ x e. On ) -> ( E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) -> ( cf ` A ) C_ x ) )
155 154 imp 
 |-  ( ( ( A e. On /\ x e. On ) /\ E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) ) -> ( cf ` A ) C_ x )
156 105 106 153 155 syl21anc 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> ( cf ` A ) C_ x )
157 ontri1 
 |-  ( ( ( cf ` A ) e. On /\ x e. On ) -> ( ( cf ` A ) C_ x <-> -. x e. ( cf ` A ) ) )
158 4 5 157 sylancr 
 |-  ( x e. ( cf ` A ) -> ( ( cf ` A ) C_ x <-> -. x e. ( cf ` A ) ) )
159 158 ad2antrr 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> ( ( cf ` A ) C_ x <-> -. x e. ( cf ` A ) ) )
160 156 159 mpbid 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> -. x e. ( cf ` A ) )
161 104 160 pm2.21dd 
 |-  ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) ) -> U_ y e. x suc ( recs ( F ) ` y ) e. A )
162 161 ex 
 |-  ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( U_ y e. x suc ( recs ( F ) ` y ) = A /\ A e. On ) -> U_ y e. x suc ( recs ( F ) ` y ) e. A ) )
163 162 expcomd 
 |-  ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( A e. On -> ( U_ y e. x suc ( recs ( F ) ` y ) = A -> U_ y e. x suc ( recs ( F ) ` y ) e. A ) ) )
164 163 com12 
 |-  ( A e. On -> ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc ( recs ( F ) ` y ) = A -> U_ y e. x suc ( recs ( F ) ` y ) e. A ) ) )
165 164 3impib 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc ( recs ( F ) ` y ) = A -> U_ y e. x suc ( recs ( F ) ` y ) e. A ) )
166 103 165 jaod 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( U_ y e. x suc ( recs ( F ) ` y ) e. A \/ U_ y e. x suc ( recs ( F ) ` y ) = A ) -> U_ y e. x suc ( recs ( F ) ` y ) e. A ) )
167 102 166 sylbid 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc ( recs ( F ) ` y ) C_ A -> U_ y e. x suc ( recs ( F ) ` y ) e. A ) )
168 89 167 mpd 
 |-  ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc ( recs ( F ) ` y ) e. A )
169 168 3adant1l 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc ( recs ( F ) ` y ) e. A )
170 ordunel 
 |-  ( ( Ord A /\ ( g ` x ) e. A /\ U_ y e. x suc ( recs ( F ) ` y ) e. A ) -> ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) e. A )
171 71 75 169 170 syl3anc 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) e. A )
172 68 171 eqeltrd 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( G ` x ) e. A )
173 172 3expia 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> ( G ` x ) e. A ) )
174 173 3impa 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> ( G ` x ) e. A ) )
175 20 174 syldc 
 |-  ( A. y e. x ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) )
176 175 a1i 
 |-  ( x e. On -> ( A. y e. x ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) ) )
177 11 176 tfis2 
 |-  ( x e. On -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) )
178 6 177 mpcom 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A )
179 178 3expia 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> ( x e. ( cf ` A ) -> ( G ` x ) e. A ) )
180 179 ralrimiv 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> A. x e. ( cf ` A ) ( G ` x ) e. A )
181 4 onssi 
 |-  ( cf ` A ) C_ On
182 fnssres 
 |-  ( ( recs ( F ) Fn On /\ ( cf ` A ) C_ On ) -> ( recs ( F ) |` ( cf ` A ) ) Fn ( cf ` A ) )
183 2 fneq1i 
 |-  ( G Fn ( cf ` A ) <-> ( recs ( F ) |` ( cf ` A ) ) Fn ( cf ` A ) )
184 182 183 sylibr 
 |-  ( ( recs ( F ) Fn On /\ ( cf ` A ) C_ On ) -> G Fn ( cf ` A ) )
185 25 181 184 mp2an 
 |-  G Fn ( cf ` A )
186 ffnfv 
 |-  ( G : ( cf ` A ) --> A <-> ( G Fn ( cf ` A ) /\ A. x e. ( cf ` A ) ( G ` x ) e. A ) )
187 185 186 mpbiran 
 |-  ( G : ( cf ` A ) --> A <-> A. x e. ( cf ` A ) ( G ` x ) e. A )
188 180 187 sylibr 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> G : ( cf ` A ) --> A )
189 188 adantlr 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> G : ( cf ` A ) --> A )
190 onss 
 |-  ( A e. On -> A C_ On )
191 190 adantl 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> A C_ On )
192 4 onordi 
 |-  Ord ( cf ` A )
193 fvex 
 |-  ( recs ( F ) ` y ) e. _V
194 193 sucid 
 |-  ( recs ( F ) ` y ) e. suc ( recs ( F ) ` y )
195 fveq2 
 |-  ( t = y -> ( recs ( F ) ` t ) = ( recs ( F ) ` y ) )
196 suceq 
 |-  ( ( recs ( F ) ` t ) = ( recs ( F ) ` y ) -> suc ( recs ( F ) ` t ) = suc ( recs ( F ) ` y ) )
197 195 196 syl 
 |-  ( t = y -> suc ( recs ( F ) ` t ) = suc ( recs ( F ) ` y ) )
198 197 eliuni 
 |-  ( ( y e. x /\ ( recs ( F ) ` y ) e. suc ( recs ( F ) ` y ) ) -> ( recs ( F ) ` y ) e. U_ t e. x suc ( recs ( F ) ` t ) )
199 198 60 eleqtrrdi 
 |-  ( ( y e. x /\ ( recs ( F ) ` y ) e. suc ( recs ( F ) ` y ) ) -> ( recs ( F ) ` y ) e. U_ y e. x suc ( recs ( F ) ` y ) )
200 194 199 mpan2 
 |-  ( y e. x -> ( recs ( F ) ` y ) e. U_ y e. x suc ( recs ( F ) ` y ) )
201 elun2 
 |-  ( ( recs ( F ) ` y ) e. U_ y e. x suc ( recs ( F ) ` y ) -> ( recs ( F ) ` y ) e. ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
202 200 201 syl 
 |-  ( y e. x -> ( recs ( F ) ` y ) e. ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
203 202 adantr 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> ( recs ( F ) ` y ) e. ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
204 5 adantl 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> x e. On )
205 204 65 syl 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> ( recs ( F ) ` x ) = ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) ) )
206 203 205 eleqtrrd 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> ( recs ( F ) ` y ) e. ( recs ( F ) ` x ) )
207 23 adantl 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> ( G ` x ) = ( recs ( F ) ` x ) )
208 206 78 207 3eltr4d 
 |-  ( ( y e. x /\ x e. ( cf ` A ) ) -> ( G ` y ) e. ( G ` x ) )
209 208 expcom 
 |-  ( x e. ( cf ` A ) -> ( y e. x -> ( G ` y ) e. ( G ` x ) ) )
210 209 ralrimiv 
 |-  ( x e. ( cf ` A ) -> A. y e. x ( G ` y ) e. ( G ` x ) )
211 210 rgen 
 |-  A. x e. ( cf ` A ) A. y e. x ( G ` y ) e. ( G ` x )
212 issmo2 
 |-  ( G : ( cf ` A ) --> A -> ( ( A C_ On /\ Ord ( cf ` A ) /\ A. x e. ( cf ` A ) A. y e. x ( G ` y ) e. ( G ` x ) ) -> Smo G ) )
213 212 com12 
 |-  ( ( A C_ On /\ Ord ( cf ` A ) /\ A. x e. ( cf ` A ) A. y e. x ( G ` y ) e. ( G ` x ) ) -> ( G : ( cf ` A ) --> A -> Smo G ) )
214 192 211 213 mp3an23 
 |-  ( A C_ On -> ( G : ( cf ` A ) --> A -> Smo G ) )
215 191 188 214 sylc 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> Smo G )
216 215 adantlr 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> Smo G )
217 fveq2 
 |-  ( x = w -> ( g ` x ) = ( g ` w ) )
218 fveq2 
 |-  ( x = w -> ( G ` x ) = ( G ` w ) )
219 217 218 sseq12d 
 |-  ( x = w -> ( ( g ` x ) C_ ( G ` x ) <-> ( g ` w ) C_ ( G ` w ) ) )
220 ssun1 
 |-  ( g ` x ) C_ ( ( g ` x ) u. U_ y e. x suc ( recs ( F ) ` y ) )
221 220 67 sseqtrrid 
 |-  ( x e. ( cf ` A ) -> ( g ` x ) C_ ( G ` x ) )
222 219 221 vtoclga 
 |-  ( w e. ( cf ` A ) -> ( g ` w ) C_ ( G ` w ) )
223 sstr 
 |-  ( ( z C_ ( g ` w ) /\ ( g ` w ) C_ ( G ` w ) ) -> z C_ ( G ` w ) )
224 223 expcom 
 |-  ( ( g ` w ) C_ ( G ` w ) -> ( z C_ ( g ` w ) -> z C_ ( G ` w ) ) )
225 222 224 syl 
 |-  ( w e. ( cf ` A ) -> ( z C_ ( g ` w ) -> z C_ ( G ` w ) ) )
226 225 reximia 
 |-  ( E. w e. ( cf ` A ) z C_ ( g ` w ) -> E. w e. ( cf ` A ) z C_ ( G ` w ) )
227 226 ralimi 
 |-  ( A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) -> A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) )
228 227 ad2antlr 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) )
229 fnex 
 |-  ( ( G Fn ( cf ` A ) /\ ( cf ` A ) e. On ) -> G e. _V )
230 185 4 229 mp2an 
 |-  G e. _V
231 feq1 
 |-  ( f = G -> ( f : ( cf ` A ) --> A <-> G : ( cf ` A ) --> A ) )
232 smoeq 
 |-  ( f = G -> ( Smo f <-> Smo G ) )
233 fveq1 
 |-  ( f = G -> ( f ` w ) = ( G ` w ) )
234 233 sseq2d 
 |-  ( f = G -> ( z C_ ( f ` w ) <-> z C_ ( G ` w ) ) )
235 234 rexbidv 
 |-  ( f = G -> ( E. w e. ( cf ` A ) z C_ ( f ` w ) <-> E. w e. ( cf ` A ) z C_ ( G ` w ) ) )
236 235 ralbidv 
 |-  ( f = G -> ( A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) <-> A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) ) )
237 231 232 236 3anbi123d 
 |-  ( f = G -> ( ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) <-> ( G : ( cf ` A ) --> A /\ Smo G /\ A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) ) ) )
238 230 237 spcev 
 |-  ( ( G : ( cf ` A ) --> A /\ Smo G /\ A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
239 189 216 228 238 syl3anc 
 |-  ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
240 239 expcom 
 |-  ( A e. On -> ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
241 240 exlimdv 
 |-  ( A e. On -> ( E. g ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
242 3 241 mpd 
 |-  ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )