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