Metamath Proof Explorer

Theorem coftr

Description: If there is a cofinal map from B to A and another from C to A , then there is also a cofinal map from C to B . Proposition 11.9 of TakeutiZaring p. 102. A limited form of transitivity for the "cof" relation. This is really a lemma for cfcof . (Contributed by Mario Carneiro, 16-Mar-2013)

Ref Expression
Hypothesis coftr.1 
|- H = ( t e. C |-> |^| { n e. B | ( g ` t ) C_ ( f ` n ) } )
Assertion coftr 
|- ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( E. g ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) ) )

Proof

Step Hyp Ref Expression
1 coftr.1 
 |-  H = ( t e. C |-> |^| { n e. B | ( g ` t ) C_ ( f ` n ) } )
2 fdm 
 |-  ( g : C --> A -> dom g = C )
3 vex 
 |-  g e. _V
4 3 dmex 
 |-  dom g e. _V
5 2 4 eqeltrrdi 
 |-  ( g : C --> A -> C e. _V )
6 fveq2 
 |-  ( t = w -> ( g ` t ) = ( g ` w ) )
7 6 sseq1d 
 |-  ( t = w -> ( ( g ` t ) C_ ( f ` n ) <-> ( g ` w ) C_ ( f ` n ) ) )
8 7 rabbidv 
 |-  ( t = w -> { n e. B | ( g ` t ) C_ ( f ` n ) } = { n e. B | ( g ` w ) C_ ( f ` n ) } )
9 8 inteqd 
 |-  ( t = w -> |^| { n e. B | ( g ` t ) C_ ( f ` n ) } = |^| { n e. B | ( g ` w ) C_ ( f ` n ) } )
10 9 cbvmptv 
 |-  ( t e. C |-> |^| { n e. B | ( g ` t ) C_ ( f ` n ) } ) = ( w e. C |-> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } )
11 1 10 eqtri 
 |-  H = ( w e. C |-> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } )
12 mptexg 
 |-  ( C e. _V -> ( w e. C |-> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } ) e. _V )
13 11 12 eqeltrid 
 |-  ( C e. _V -> H e. _V )
14 5 13 syl 
 |-  ( g : C --> A -> H e. _V )
15 14 ad2antrl 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> H e. _V )
16 ffn 
 |-  ( f : B --> A -> f Fn B )
17 smodm2 
 |-  ( ( f Fn B /\ Smo f ) -> Ord B )
18 16 17 sylan 
 |-  ( ( f : B --> A /\ Smo f ) -> Ord B )
19 18 3adant3 
 |-  ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> Ord B )
20 19 adantr 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> Ord B )
21 simpl3 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> A. x e. A E. y e. B x C_ ( f ` y ) )
22 simprl 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> g : C --> A )
23 simpl1 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> Ord B )
24 simpl2 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> A. x e. A E. y e. B x C_ ( f ` y ) )
25 ffvelrn 
 |-  ( ( g : C --> A /\ w e. C ) -> ( g ` w ) e. A )
26 25 3ad2antl3 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> ( g ` w ) e. A )
27 sseq1 
 |-  ( x = ( g ` w ) -> ( x C_ ( f ` y ) <-> ( g ` w ) C_ ( f ` y ) ) )
28 27 rexbidv 
 |-  ( x = ( g ` w ) -> ( E. y e. B x C_ ( f ` y ) <-> E. y e. B ( g ` w ) C_ ( f ` y ) ) )
29 28 rspccv 
 |-  ( A. x e. A E. y e. B x C_ ( f ` y ) -> ( ( g ` w ) e. A -> E. y e. B ( g ` w ) C_ ( f ` y ) ) )
30 24 26 29 sylc 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> E. y e. B ( g ` w ) C_ ( f ` y ) )
31 ssrab2 
 |-  { n e. B | ( g ` w ) C_ ( f ` n ) } C_ B
32 ordsson 
 |-  ( Ord B -> B C_ On )
33 31 32 sstrid 
 |-  ( Ord B -> { n e. B | ( g ` w ) C_ ( f ` n ) } C_ On )
34 fveq2 
 |-  ( n = y -> ( f ` n ) = ( f ` y ) )
35 34 sseq2d 
 |-  ( n = y -> ( ( g ` w ) C_ ( f ` n ) <-> ( g ` w ) C_ ( f ` y ) ) )
36 35 rspcev 
 |-  ( ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) -> E. n e. B ( g ` w ) C_ ( f ` n ) )
37 rabn0 
 |-  ( { n e. B | ( g ` w ) C_ ( f ` n ) } =/= (/) <-> E. n e. B ( g ` w ) C_ ( f ` n ) )
38 36 37 sylibr 
 |-  ( ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) -> { n e. B | ( g ` w ) C_ ( f ` n ) } =/= (/) )
39 oninton 
 |-  ( ( { n e. B | ( g ` w ) C_ ( f ` n ) } C_ On /\ { n e. B | ( g ` w ) C_ ( f ` n ) } =/= (/) ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. On )
40 33 38 39 syl2an 
 |-  ( ( Ord B /\ ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. On )
41 eloni 
 |-  ( |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. On -> Ord |^| { n e. B | ( g ` w ) C_ ( f ` n ) } )
42 40 41 syl 
 |-  ( ( Ord B /\ ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) ) -> Ord |^| { n e. B | ( g ` w ) C_ ( f ` n ) } )
43 simpl 
 |-  ( ( Ord B /\ ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) ) -> Ord B )
44 35 intminss 
 |-  ( ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } C_ y )
45 44 adantl 
 |-  ( ( Ord B /\ ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } C_ y )
46 simprl 
 |-  ( ( Ord B /\ ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) ) -> y e. B )
47 ordtr2 
 |-  ( ( Ord |^| { n e. B | ( g ` w ) C_ ( f ` n ) } /\ Ord B ) -> ( ( |^| { n e. B | ( g ` w ) C_ ( f ` n ) } C_ y /\ y e. B ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B ) )
48 47 imp 
 |-  ( ( ( Ord |^| { n e. B | ( g ` w ) C_ ( f ` n ) } /\ Ord B ) /\ ( |^| { n e. B | ( g ` w ) C_ ( f ` n ) } C_ y /\ y e. B ) ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B )
49 42 43 45 46 48 syl22anc 
 |-  ( ( Ord B /\ ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B )
50 49 rexlimdvaa 
 |-  ( Ord B -> ( E. y e. B ( g ` w ) C_ ( f ` y ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B ) )
51 23 30 50 sylc 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B )
52 51 11 fmptd 
 |-  ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) -> H : C --> B )
53 20 21 22 52 syl3anc 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> H : C --> B )
54 simprr 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> A. z e. A E. w e. C z C_ ( g ` w ) )
55 simpl1 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> f : B --> A )
56 ffvelrn 
 |-  ( ( f : B --> A /\ s e. B ) -> ( f ` s ) e. A )
57 sseq1 
 |-  ( z = ( f ` s ) -> ( z C_ ( g ` w ) <-> ( f ` s ) C_ ( g ` w ) ) )
58 57 rexbidv 
 |-  ( z = ( f ` s ) -> ( E. w e. C z C_ ( g ` w ) <-> E. w e. C ( f ` s ) C_ ( g ` w ) ) )
59 58 rspccv 
 |-  ( A. z e. A E. w e. C z C_ ( g ` w ) -> ( ( f ` s ) e. A -> E. w e. C ( f ` s ) C_ ( g ` w ) ) )
60 56 59 syl5 
 |-  ( A. z e. A E. w e. C z C_ ( g ` w ) -> ( ( f : B --> A /\ s e. B ) -> E. w e. C ( f ` s ) C_ ( g ` w ) ) )
61 60 expdimp 
 |-  ( ( A. z e. A E. w e. C z C_ ( g ` w ) /\ f : B --> A ) -> ( s e. B -> E. w e. C ( f ` s ) C_ ( g ` w ) ) )
62 54 55 61 syl2anc 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> ( s e. B -> E. w e. C ( f ` s ) C_ ( g ` w ) ) )
63 55 16 syl 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> f Fn B )
64 simpl2 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> Smo f )
65 simpr 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> w e. C )
66 65 51 jca 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> ( w e. C /\ |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B ) )
67 35 elrab 
 |-  ( y e. { n e. B | ( g ` w ) C_ ( f ` n ) } <-> ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) )
68 sstr2 
 |-  ( ( f ` s ) C_ ( g ` w ) -> ( ( g ` w ) C_ ( f ` y ) -> ( f ` s ) C_ ( f ` y ) ) )
69 smoword 
 |-  ( ( ( f Fn B /\ Smo f ) /\ ( s e. B /\ y e. B ) ) -> ( s C_ y <-> ( f ` s ) C_ ( f ` y ) ) )
70 69 biimprd 
 |-  ( ( ( f Fn B /\ Smo f ) /\ ( s e. B /\ y e. B ) ) -> ( ( f ` s ) C_ ( f ` y ) -> s C_ y ) )
71 68 70 syl9r 
 |-  ( ( ( f Fn B /\ Smo f ) /\ ( s e. B /\ y e. B ) ) -> ( ( f ` s ) C_ ( g ` w ) -> ( ( g ` w ) C_ ( f ` y ) -> s C_ y ) ) )
72 71 expr 
 |-  ( ( ( f Fn B /\ Smo f ) /\ s e. B ) -> ( y e. B -> ( ( f ` s ) C_ ( g ` w ) -> ( ( g ` w ) C_ ( f ` y ) -> s C_ y ) ) ) )
73 72 com23 
 |-  ( ( ( f Fn B /\ Smo f ) /\ s e. B ) -> ( ( f ` s ) C_ ( g ` w ) -> ( y e. B -> ( ( g ` w ) C_ ( f ` y ) -> s C_ y ) ) ) )
74 73 imp4b 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( f ` s ) C_ ( g ` w ) ) -> ( ( y e. B /\ ( g ` w ) C_ ( f ` y ) ) -> s C_ y ) )
75 67 74 syl5bi 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( f ` s ) C_ ( g ` w ) ) -> ( y e. { n e. B | ( g ` w ) C_ ( f ` n ) } -> s C_ y ) )
76 75 ralrimiv 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( f ` s ) C_ ( g ` w ) ) -> A. y e. { n e. B | ( g ` w ) C_ ( f ` n ) } s C_ y )
77 ssint 
 |-  ( s C_ |^| { n e. B | ( g ` w ) C_ ( f ` n ) } <-> A. y e. { n e. B | ( g ` w ) C_ ( f ` n ) } s C_ y )
78 76 77 sylibr 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( f ` s ) C_ ( g ` w ) ) -> s C_ |^| { n e. B | ( g ` w ) C_ ( f ` n ) } )
79 9 1 fvmptg 
 |-  ( ( w e. C /\ |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B ) -> ( H ` w ) = |^| { n e. B | ( g ` w ) C_ ( f ` n ) } )
80 79 sseq2d 
 |-  ( ( w e. C /\ |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B ) -> ( s C_ ( H ` w ) <-> s C_ |^| { n e. B | ( g ` w ) C_ ( f ` n ) } ) )
81 78 80 syl5ibrcom 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( f ` s ) C_ ( g ` w ) ) -> ( ( w e. C /\ |^| { n e. B | ( g ` w ) C_ ( f ` n ) } e. B ) -> s C_ ( H ` w ) ) )
82 66 81 syl5 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( f ` s ) C_ ( g ` w ) ) -> ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> s C_ ( H ` w ) ) )
83 82 ex 
 |-  ( ( ( f Fn B /\ Smo f ) /\ s e. B ) -> ( ( f ` s ) C_ ( g ` w ) -> ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> s C_ ( H ` w ) ) ) )
84 83 com23 
 |-  ( ( ( f Fn B /\ Smo f ) /\ s e. B ) -> ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ w e. C ) -> ( ( f ` s ) C_ ( g ` w ) -> s C_ ( H ` w ) ) ) )
85 84 expdimp 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) ) -> ( w e. C -> ( ( f ` s ) C_ ( g ` w ) -> s C_ ( H ` w ) ) ) )
86 85 reximdvai 
 |-  ( ( ( ( f Fn B /\ Smo f ) /\ s e. B ) /\ ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) ) -> ( E. w e. C ( f ` s ) C_ ( g ` w ) -> E. w e. C s C_ ( H ` w ) ) )
87 86 ancoms 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ ( ( f Fn B /\ Smo f ) /\ s e. B ) ) -> ( E. w e. C ( f ` s ) C_ ( g ` w ) -> E. w e. C s C_ ( H ` w ) ) )
88 87 expr 
 |-  ( ( ( Ord B /\ A. x e. A E. y e. B x C_ ( f ` y ) /\ g : C --> A ) /\ ( f Fn B /\ Smo f ) ) -> ( s e. B -> ( E. w e. C ( f ` s ) C_ ( g ` w ) -> E. w e. C s C_ ( H ` w ) ) ) )
89 20 21 22 63 64 88 syl32anc 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> ( s e. B -> ( E. w e. C ( f ` s ) C_ ( g ` w ) -> E. w e. C s C_ ( H ` w ) ) ) )
90 62 89 mpdd 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> ( s e. B -> E. w e. C s C_ ( H ` w ) ) )
91 90 ralrimiv 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> A. s e. B E. w e. C s C_ ( H ` w ) )
92 feq1 
 |-  ( h = H -> ( h : C --> B <-> H : C --> B ) )
93 fveq1 
 |-  ( h = H -> ( h ` w ) = ( H ` w ) )
94 93 sseq2d 
 |-  ( h = H -> ( s C_ ( h ` w ) <-> s C_ ( H ` w ) ) )
95 94 rexbidv 
 |-  ( h = H -> ( E. w e. C s C_ ( h ` w ) <-> E. w e. C s C_ ( H ` w ) ) )
96 95 ralbidv 
 |-  ( h = H -> ( A. s e. B E. w e. C s C_ ( h ` w ) <-> A. s e. B E. w e. C s C_ ( H ` w ) ) )
97 92 96 anbi12d 
 |-  ( h = H -> ( ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) <-> ( H : C --> B /\ A. s e. B E. w e. C s C_ ( H ` w ) ) ) )
98 97 spcegv 
 |-  ( H e. _V -> ( ( H : C --> B /\ A. s e. B E. w e. C s C_ ( H ` w ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) ) )
99 98 3impib 
 |-  ( ( H e. _V /\ H : C --> B /\ A. s e. B E. w e. C s C_ ( H ` w ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) )
100 15 53 91 99 syl3anc 
 |-  ( ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) /\ ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) )
101 100 ex 
 |-  ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) ) )
102 101 exlimdv 
 |-  ( ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( E. g ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) ) )
103 102 exlimiv 
 |-  ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( E. g ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) ) )