Metamath Proof Explorer

Theorem cfcoflem

Description: Lemma for cfcof , showing subset relation in one direction. (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Assertion cfcoflem 
|- ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( cf ` A ) C_ ( cf ` B ) ) )

Proof

Step Hyp Ref Expression
1 cff1 
 |-  ( B e. On -> E. g ( g : ( cf ` B ) -1-1-> B /\ A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) ) )
2 f1f 
 |-  ( g : ( cf ` B ) -1-1-> B -> g : ( cf ` B ) --> B )
3 fco 
 |-  ( ( f : B --> A /\ g : ( cf ` B ) --> B ) -> ( f o. g ) : ( cf ` B ) --> A )
4 3 adantlr 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( f o. g ) : ( cf ` B ) --> A )
5 r19.29 
 |-  ( ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) /\ E. y e. B x C_ ( f ` y ) ) -> E. y e. B ( E. z e. ( cf ` B ) y C_ ( g ` z ) /\ x C_ ( f ` y ) ) )
6 ffvelrn 
 |-  ( ( g : ( cf ` B ) --> B /\ z e. ( cf ` B ) ) -> ( g ` z ) e. B )
7 ffn 
 |-  ( f : B --> A -> f Fn B )
8 smoword 
 |-  ( ( ( f Fn B /\ Smo f ) /\ ( y e. B /\ ( g ` z ) e. B ) ) -> ( y C_ ( g ` z ) <-> ( f ` y ) C_ ( f ` ( g ` z ) ) ) )
9 8 biimpd 
 |-  ( ( ( f Fn B /\ Smo f ) /\ ( y e. B /\ ( g ` z ) e. B ) ) -> ( y C_ ( g ` z ) -> ( f ` y ) C_ ( f ` ( g ` z ) ) ) )
10 9 exp32 
 |-  ( ( f Fn B /\ Smo f ) -> ( y e. B -> ( ( g ` z ) e. B -> ( y C_ ( g ` z ) -> ( f ` y ) C_ ( f ` ( g ` z ) ) ) ) ) )
11 7 10 sylan 
 |-  ( ( f : B --> A /\ Smo f ) -> ( y e. B -> ( ( g ` z ) e. B -> ( y C_ ( g ` z ) -> ( f ` y ) C_ ( f ` ( g ` z ) ) ) ) ) )
12 6 11 syl7 
 |-  ( ( f : B --> A /\ Smo f ) -> ( y e. B -> ( ( g : ( cf ` B ) --> B /\ z e. ( cf ` B ) ) -> ( y C_ ( g ` z ) -> ( f ` y ) C_ ( f ` ( g ` z ) ) ) ) ) )
13 12 com23 
 |-  ( ( f : B --> A /\ Smo f ) -> ( ( g : ( cf ` B ) --> B /\ z e. ( cf ` B ) ) -> ( y e. B -> ( y C_ ( g ` z ) -> ( f ` y ) C_ ( f ` ( g ` z ) ) ) ) ) )
14 13 expdimp 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( z e. ( cf ` B ) -> ( y e. B -> ( y C_ ( g ` z ) -> ( f ` y ) C_ ( f ` ( g ` z ) ) ) ) ) )
15 14 3imp2 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ ( z e. ( cf ` B ) /\ y e. B /\ y C_ ( g ` z ) ) ) -> ( f ` y ) C_ ( f ` ( g ` z ) ) )
16 sstr2 
 |-  ( x C_ ( f ` y ) -> ( ( f ` y ) C_ ( f ` ( g ` z ) ) -> x C_ ( f ` ( g ` z ) ) ) )
17 15 16 syl5com 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ ( z e. ( cf ` B ) /\ y e. B /\ y C_ ( g ` z ) ) ) -> ( x C_ ( f ` y ) -> x C_ ( f ` ( g ` z ) ) ) )
18 fvco3 
 |-  ( ( g : ( cf ` B ) --> B /\ z e. ( cf ` B ) ) -> ( ( f o. g ) ` z ) = ( f ` ( g ` z ) ) )
19 18 sseq2d 
 |-  ( ( g : ( cf ` B ) --> B /\ z e. ( cf ` B ) ) -> ( x C_ ( ( f o. g ) ` z ) <-> x C_ ( f ` ( g ` z ) ) ) )
20 19 adantll 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ z e. ( cf ` B ) ) -> ( x C_ ( ( f o. g ) ` z ) <-> x C_ ( f ` ( g ` z ) ) ) )
21 20 3ad2antr1 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ ( z e. ( cf ` B ) /\ y e. B /\ y C_ ( g ` z ) ) ) -> ( x C_ ( ( f o. g ) ` z ) <-> x C_ ( f ` ( g ` z ) ) ) )
22 17 21 sylibrd 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ ( z e. ( cf ` B ) /\ y e. B /\ y C_ ( g ` z ) ) ) -> ( x C_ ( f ` y ) -> x C_ ( ( f o. g ) ` z ) ) )
23 22 expcom 
 |-  ( ( z e. ( cf ` B ) /\ y e. B /\ y C_ ( g ` z ) ) -> ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( x C_ ( f ` y ) -> x C_ ( ( f o. g ) ` z ) ) ) )
24 23 3expia 
 |-  ( ( z e. ( cf ` B ) /\ y e. B ) -> ( y C_ ( g ` z ) -> ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( x C_ ( f ` y ) -> x C_ ( ( f o. g ) ` z ) ) ) ) )
25 24 com4t 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( x C_ ( f ` y ) -> ( ( z e. ( cf ` B ) /\ y e. B ) -> ( y C_ ( g ` z ) -> x C_ ( ( f o. g ) ` z ) ) ) ) )
26 25 imp 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ x C_ ( f ` y ) ) -> ( ( z e. ( cf ` B ) /\ y e. B ) -> ( y C_ ( g ` z ) -> x C_ ( ( f o. g ) ` z ) ) ) )
27 26 expcomd 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ x C_ ( f ` y ) ) -> ( y e. B -> ( z e. ( cf ` B ) -> ( y C_ ( g ` z ) -> x C_ ( ( f o. g ) ` z ) ) ) ) )
28 27 imp31 
 |-  ( ( ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ x C_ ( f ` y ) ) /\ y e. B ) /\ z e. ( cf ` B ) ) -> ( y C_ ( g ` z ) -> x C_ ( ( f o. g ) ` z ) ) )
29 28 reximdva 
 |-  ( ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ x C_ ( f ` y ) ) /\ y e. B ) -> ( E. z e. ( cf ` B ) y C_ ( g ` z ) -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) )
30 29 exp31 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( x C_ ( f ` y ) -> ( y e. B -> ( E. z e. ( cf ` B ) y C_ ( g ` z ) -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) ) ) )
31 30 com34 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( x C_ ( f ` y ) -> ( E. z e. ( cf ` B ) y C_ ( g ` z ) -> ( y e. B -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) ) ) )
32 31 impcomd 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( ( E. z e. ( cf ` B ) y C_ ( g ` z ) /\ x C_ ( f ` y ) ) -> ( y e. B -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) ) )
33 32 com23 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( y e. B -> ( ( E. z e. ( cf ` B ) y C_ ( g ` z ) /\ x C_ ( f ` y ) ) -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) ) )
34 33 rexlimdv 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( E. y e. B ( E. z e. ( cf ` B ) y C_ ( g ` z ) /\ x C_ ( f ` y ) ) -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) )
35 5 34 syl5 
 |-  ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) -> ( ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) /\ E. y e. B x C_ ( f ` y ) ) -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) )
36 35 expdimp 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) ) -> ( E. y e. B x C_ ( f ` y ) -> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) )
37 36 ralimdv 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) ) -> ( A. x e. A E. y e. B x C_ ( f ` y ) -> A. x e. A E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) )
38 37 impr 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) /\ A. x e. A E. y e. B x C_ ( f ` y ) ) ) -> A. x e. A E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) )
39 vex 
 |-  f e. _V
40 vex 
 |-  g e. _V
41 39 40 coex 
 |-  ( f o. g ) e. _V
42 feq1 
 |-  ( h = ( f o. g ) -> ( h : ( cf ` B ) --> A <-> ( f o. g ) : ( cf ` B ) --> A ) )
43 fveq1 
 |-  ( h = ( f o. g ) -> ( h ` z ) = ( ( f o. g ) ` z ) )
44 43 sseq2d 
 |-  ( h = ( f o. g ) -> ( x C_ ( h ` z ) <-> x C_ ( ( f o. g ) ` z ) ) )
45 44 rexbidv 
 |-  ( h = ( f o. g ) -> ( E. z e. ( cf ` B ) x C_ ( h ` z ) <-> E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) )
46 45 ralbidv 
 |-  ( h = ( f o. g ) -> ( A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) <-> A. x e. A E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) )
47 42 46 anbi12d 
 |-  ( h = ( f o. g ) -> ( ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) <-> ( ( f o. g ) : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) ) )
48 41 47 spcev 
 |-  ( ( ( f o. g ) : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( ( f o. g ) ` z ) ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) )
49 4 38 48 syl2an2r 
 |-  ( ( ( ( f : B --> A /\ Smo f ) /\ g : ( cf ` B ) --> B ) /\ ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) /\ A. x e. A E. y e. B x C_ ( f ` y ) ) ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) )
50 49 exp43 
 |-  ( ( f : B --> A /\ Smo f ) -> ( g : ( cf ` B ) --> B -> ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) -> ( A. x e. A E. y e. B x C_ ( f ` y ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) ) ) )
51 50 com24 
 |-  ( ( f : B --> A /\ Smo f ) -> ( A. x e. A E. y e. B x C_ ( f ` y ) -> ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) -> ( g : ( cf ` B ) --> B -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) ) ) )
52 51 3impia 
 |-  ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) -> ( g : ( cf ` B ) --> B -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) ) )
53 52 exlimiv 
 |-  ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) -> ( g : ( cf ` B ) --> B -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) ) )
54 53 com13 
 |-  ( g : ( cf ` B ) --> B -> ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) ) )
55 2 54 syl 
 |-  ( g : ( cf ` B ) -1-1-> B -> ( A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) ) )
56 55 imp 
 |-  ( ( g : ( cf ` B ) -1-1-> B /\ A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) ) -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) )
57 56 exlimiv 
 |-  ( E. g ( g : ( cf ` B ) -1-1-> B /\ A. y e. B E. z e. ( cf ` B ) y C_ ( g ` z ) ) -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) )
58 1 57 syl 
 |-  ( B e. On -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) ) )
59 cfon 
 |-  ( cf ` B ) e. On
60 cfflb 
 |-  ( ( A e. On /\ ( cf ` B ) e. On ) -> ( E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) -> ( cf ` A ) C_ ( cf ` B ) ) )
61 59 60 mpan2 
 |-  ( A e. On -> ( E. h ( h : ( cf ` B ) --> A /\ A. x e. A E. z e. ( cf ` B ) x C_ ( h ` z ) ) -> ( cf ` A ) C_ ( cf ` B ) ) )
62 58 61 sylan9r 
 |-  ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( cf ` A ) C_ ( cf ` B ) ) )