Metamath Proof Explorer

Theorem txcmplem1

Description: Lemma for txcmp . (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses txcmp.x 
|- X = U. R
txcmp.y 
|- Y = U. S
txcmp.r 
|- ( ph -> R e. Comp )
txcmp.s 
|- ( ph -> S e. Comp )
txcmp.w 
|- ( ph -> W C_ ( R tX S ) )
txcmp.u 
|- ( ph -> ( X X. Y ) = U. W )
txcmp.a 
|- ( ph -> A e. Y )
Assertion txcmplem1 
|- ( ph -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )

Proof

Step Hyp Ref Expression
1 txcmp.x 
 |-  X = U. R
2 txcmp.y 
 |-  Y = U. S
3 txcmp.r 
 |-  ( ph -> R e. Comp )
4 txcmp.s 
 |-  ( ph -> S e. Comp )
5 txcmp.w 
 |-  ( ph -> W C_ ( R tX S ) )
6 txcmp.u 
 |-  ( ph -> ( X X. Y ) = U. W )
7 txcmp.a 
 |-  ( ph -> A e. Y )
8 id 
 |-  ( x e. X -> x e. X )
9 opelxpi 
 |-  ( ( x e. X /\ A e. Y ) -> <. x , A >. e. ( X X. Y ) )
10 8 7 9 syl2anr 
 |-  ( ( ph /\ x e. X ) -> <. x , A >. e. ( X X. Y ) )
11 6 adantr 
 |-  ( ( ph /\ x e. X ) -> ( X X. Y ) = U. W )
12 10 11 eleqtrd 
 |-  ( ( ph /\ x e. X ) -> <. x , A >. e. U. W )
13 eluni2 
 |-  ( <. x , A >. e. U. W <-> E. k e. W <. x , A >. e. k )
14 12 13 sylib 
 |-  ( ( ph /\ x e. X ) -> E. k e. W <. x , A >. e. k )
15 5 adantr 
 |-  ( ( ph /\ x e. X ) -> W C_ ( R tX S ) )
16 15 sselda 
 |-  ( ( ( ph /\ x e. X ) /\ k e. W ) -> k e. ( R tX S ) )
17 eltx 
 |-  ( ( R e. Comp /\ S e. Comp ) -> ( k e. ( R tX S ) <-> A. y e. k E. r e. R E. s e. S ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) ) )
18 3 4 17 syl2anc 
 |-  ( ph -> ( k e. ( R tX S ) <-> A. y e. k E. r e. R E. s e. S ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) ) )
19 18 adantr 
 |-  ( ( ph /\ x e. X ) -> ( k e. ( R tX S ) <-> A. y e. k E. r e. R E. s e. S ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) ) )
20 19 biimpa 
 |-  ( ( ( ph /\ x e. X ) /\ k e. ( R tX S ) ) -> A. y e. k E. r e. R E. s e. S ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) )
21 16 20 syldan 
 |-  ( ( ( ph /\ x e. X ) /\ k e. W ) -> A. y e. k E. r e. R E. s e. S ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) )
22 eleq1 
 |-  ( y = <. x , A >. -> ( y e. ( r X. s ) <-> <. x , A >. e. ( r X. s ) ) )
23 22 anbi1d 
 |-  ( y = <. x , A >. -> ( ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) <-> ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) )
24 23 2rexbidv 
 |-  ( y = <. x , A >. -> ( E. r e. R E. s e. S ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) <-> E. r e. R E. s e. S ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) )
25 24 rspccv 
 |-  ( A. y e. k E. r e. R E. s e. S ( y e. ( r X. s ) /\ ( r X. s ) C_ k ) -> ( <. x , A >. e. k -> E. r e. R E. s e. S ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) )
26 21 25 syl 
 |-  ( ( ( ph /\ x e. X ) /\ k e. W ) -> ( <. x , A >. e. k -> E. r e. R E. s e. S ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) )
27 opelxp1 
 |-  ( <. x , A >. e. ( r X. s ) -> x e. r )
28 27 ad2antrl 
 |-  ( ( ( ( ph /\ x e. X ) /\ k e. W ) /\ ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) -> x e. r )
29 opelxp2 
 |-  ( <. x , A >. e. ( r X. s ) -> A e. s )
30 29 ad2antrl 
 |-  ( ( ( ( ph /\ x e. X ) /\ k e. W ) /\ ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) -> A e. s )
31 30 snssd 
 |-  ( ( ( ( ph /\ x e. X ) /\ k e. W ) /\ ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) -> { A } C_ s )
32 xpss2 
 |-  ( { A } C_ s -> ( r X. { A } ) C_ ( r X. s ) )
33 31 32 syl 
 |-  ( ( ( ( ph /\ x e. X ) /\ k e. W ) /\ ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) -> ( r X. { A } ) C_ ( r X. s ) )
34 simprr 
 |-  ( ( ( ( ph /\ x e. X ) /\ k e. W ) /\ ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) -> ( r X. s ) C_ k )
35 33 34 sstrd 
 |-  ( ( ( ( ph /\ x e. X ) /\ k e. W ) /\ ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) -> ( r X. { A } ) C_ k )
36 28 35 jca 
 |-  ( ( ( ( ph /\ x e. X ) /\ k e. W ) /\ ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) ) -> ( x e. r /\ ( r X. { A } ) C_ k ) )
37 36 ex 
 |-  ( ( ( ph /\ x e. X ) /\ k e. W ) -> ( ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) -> ( x e. r /\ ( r X. { A } ) C_ k ) ) )
38 37 rexlimdvw 
 |-  ( ( ( ph /\ x e. X ) /\ k e. W ) -> ( E. s e. S ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) -> ( x e. r /\ ( r X. { A } ) C_ k ) ) )
39 38 reximdv 
 |-  ( ( ( ph /\ x e. X ) /\ k e. W ) -> ( E. r e. R E. s e. S ( <. x , A >. e. ( r X. s ) /\ ( r X. s ) C_ k ) -> E. r e. R ( x e. r /\ ( r X. { A } ) C_ k ) ) )
40 26 39 syld 
 |-  ( ( ( ph /\ x e. X ) /\ k e. W ) -> ( <. x , A >. e. k -> E. r e. R ( x e. r /\ ( r X. { A } ) C_ k ) ) )
41 40 reximdva 
 |-  ( ( ph /\ x e. X ) -> ( E. k e. W <. x , A >. e. k -> E. k e. W E. r e. R ( x e. r /\ ( r X. { A } ) C_ k ) ) )
42 14 41 mpd 
 |-  ( ( ph /\ x e. X ) -> E. k e. W E. r e. R ( x e. r /\ ( r X. { A } ) C_ k ) )
43 rexcom 
 |-  ( E. k e. W E. r e. R ( x e. r /\ ( r X. { A } ) C_ k ) <-> E. r e. R E. k e. W ( x e. r /\ ( r X. { A } ) C_ k ) )
44 r19.42v 
 |-  ( E. k e. W ( x e. r /\ ( r X. { A } ) C_ k ) <-> ( x e. r /\ E. k e. W ( r X. { A } ) C_ k ) )
45 44 rexbii 
 |-  ( E. r e. R E. k e. W ( x e. r /\ ( r X. { A } ) C_ k ) <-> E. r e. R ( x e. r /\ E. k e. W ( r X. { A } ) C_ k ) )
46 43 45 bitri 
 |-  ( E. k e. W E. r e. R ( x e. r /\ ( r X. { A } ) C_ k ) <-> E. r e. R ( x e. r /\ E. k e. W ( r X. { A } ) C_ k ) )
47 42 46 sylib 
 |-  ( ( ph /\ x e. X ) -> E. r e. R ( x e. r /\ E. k e. W ( r X. { A } ) C_ k ) )
48 47 ralrimiva 
 |-  ( ph -> A. x e. X E. r e. R ( x e. r /\ E. k e. W ( r X. { A } ) C_ k ) )
49 sseq2 
 |-  ( k = ( f ` r ) -> ( ( r X. { A } ) C_ k <-> ( r X. { A } ) C_ ( f ` r ) ) )
50 1 49 cmpcovf 
 |-  ( ( R e. Comp /\ A. x e. X E. r e. R ( x e. r /\ E. k e. W ( r X. { A } ) C_ k ) ) -> E. t e. ( ~P R i^i Fin ) ( X = U. t /\ E. f ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) )
51 3 48 50 syl2anc 
 |-  ( ph -> E. t e. ( ~P R i^i Fin ) ( X = U. t /\ E. f ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) )
52 3 ad2antrr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> R e. Comp )
53 cmptop 
 |-  ( S e. Comp -> S e. Top )
54 4 53 syl 
 |-  ( ph -> S e. Top )
55 54 ad2antrr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> S e. Top )
56 cmptop 
 |-  ( R e. Comp -> R e. Top )
57 52 56 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> R e. Top )
58 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
59 57 55 58 syl2anc 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ( R tX S ) e. Top )
60 simprrl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> f : t --> W )
61 60 frnd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ran f C_ W )
62 5 ad2antrr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> W C_ ( R tX S ) )
63 61 62 sstrd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ran f C_ ( R tX S ) )
64 uniopn 
 |-  ( ( ( R tX S ) e. Top /\ ran f C_ ( R tX S ) ) -> U. ran f e. ( R tX S ) )
65 59 63 64 syl2anc 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> U. ran f e. ( R tX S ) )
66 simprrr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> A. r e. t ( r X. { A } ) C_ ( f ` r ) )
67 ss2iun 
 |-  ( A. r e. t ( r X. { A } ) C_ ( f ` r ) -> U_ r e. t ( r X. { A } ) C_ U_ r e. t ( f ` r ) )
68 66 67 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> U_ r e. t ( r X. { A } ) C_ U_ r e. t ( f ` r ) )
69 simprl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> X = U. t )
70 uniiun 
 |-  U. t = U_ r e. t r
71 69 70 eqtrdi 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> X = U_ r e. t r )
72 71 xpeq1d 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ( X X. { A } ) = ( U_ r e. t r X. { A } ) )
73 xpiundir 
 |-  ( U_ r e. t r X. { A } ) = U_ r e. t ( r X. { A } )
74 72 73 eqtr2di 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> U_ r e. t ( r X. { A } ) = ( X X. { A } ) )
75 60 ffnd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> f Fn t )
76 fniunfv 
 |-  ( f Fn t -> U_ r e. t ( f ` r ) = U. ran f )
77 75 76 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> U_ r e. t ( f ` r ) = U. ran f )
78 68 74 77 3sstr3d 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ( X X. { A } ) C_ U. ran f )
79 7 ad2antrr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> A e. Y )
80 1 2 52 55 65 78 79 txtube 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> E. u e. S ( A e. u /\ ( X X. u ) C_ U. ran f ) )
81 vex 
 |-  f e. _V
82 81 rnex 
 |-  ran f e. _V
83 82 elpw 
 |-  ( ran f e. ~P W <-> ran f C_ W )
84 61 83 sylibr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ran f e. ~P W )
85 simplr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> t e. ( ~P R i^i Fin ) )
86 85 elin2d 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> t e. Fin )
87 dffn4 
 |-  ( f Fn t <-> f : t -onto-> ran f )
88 75 87 sylib 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> f : t -onto-> ran f )
89 fofi 
 |-  ( ( t e. Fin /\ f : t -onto-> ran f ) -> ran f e. Fin )
90 86 88 89 syl2anc 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ran f e. Fin )
91 84 90 elind 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ran f e. ( ~P W i^i Fin ) )
92 unieq 
 |-  ( v = ran f -> U. v = U. ran f )
93 92 sseq2d 
 |-  ( v = ran f -> ( ( X X. u ) C_ U. v <-> ( X X. u ) C_ U. ran f ) )
94 93 rspcev 
 |-  ( ( ran f e. ( ~P W i^i Fin ) /\ ( X X. u ) C_ U. ran f ) -> E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v )
95 94 ex 
 |-  ( ran f e. ( ~P W i^i Fin ) -> ( ( X X. u ) C_ U. ran f -> E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )
96 91 95 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ( ( X X. u ) C_ U. ran f -> E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )
97 96 anim2d 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ( ( A e. u /\ ( X X. u ) C_ U. ran f ) -> ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) ) )
98 97 reximdv 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> ( E. u e. S ( A e. u /\ ( X X. u ) C_ U. ran f ) -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) ) )
99 80 98 mpd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) ) -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )
100 99 expr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ X = U. t ) -> ( ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) ) )
101 100 exlimdv 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ X = U. t ) -> ( E. f ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) ) )
102 101 expimpd 
 |-  ( ( ph /\ t e. ( ~P R i^i Fin ) ) -> ( ( X = U. t /\ E. f ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) ) )
103 102 rexlimdva 
 |-  ( ph -> ( E. t e. ( ~P R i^i Fin ) ( X = U. t /\ E. f ( f : t --> W /\ A. r e. t ( r X. { A } ) C_ ( f ` r ) ) ) -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) ) )
104 51 103 mpd 
 |-  ( ph -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )