Metamath Proof Explorer

Theorem txcmplem2

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 )
Assertion txcmplem2 
|- ( ph -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = 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 3 adantr 
 |-  ( ( ph /\ x e. Y ) -> R e. Comp )
8 4 adantr 
 |-  ( ( ph /\ x e. Y ) -> S e. Comp )
9 5 adantr 
 |-  ( ( ph /\ x e. Y ) -> W C_ ( R tX S ) )
10 6 adantr 
 |-  ( ( ph /\ x e. Y ) -> ( X X. Y ) = U. W )
11 simpr 
 |-  ( ( ph /\ x e. Y ) -> x e. Y )
12 1 2 7 8 9 10 11 txcmplem1 
 |-  ( ( ph /\ x e. Y ) -> E. u e. S ( x e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )
13 12 ralrimiva 
 |-  ( ph -> A. x e. Y E. u e. S ( x e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )
14 unieq 
 |-  ( v = ( f ` u ) -> U. v = U. ( f ` u ) )
15 14 sseq2d 
 |-  ( v = ( f ` u ) -> ( ( X X. u ) C_ U. v <-> ( X X. u ) C_ U. ( f ` u ) ) )
16 2 15 cmpcovf 
 |-  ( ( S e. Comp /\ A. x e. Y E. u e. S ( x e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) ) -> E. w e. ( ~P S i^i Fin ) ( Y = U. w /\ E. f ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) )
17 4 13 16 syl2anc 
 |-  ( ph -> E. w e. ( ~P S i^i Fin ) ( Y = U. w /\ E. f ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) )
18 simprrl 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> f : w --> ( ~P W i^i Fin ) )
19 ffn 
 |-  ( f : w --> ( ~P W i^i Fin ) -> f Fn w )
20 fniunfv 
 |-  ( f Fn w -> U_ z e. w ( f ` z ) = U. ran f )
21 18 19 20 3syl 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U_ z e. w ( f ` z ) = U. ran f )
22 18 frnd 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> ran f C_ ( ~P W i^i Fin ) )
23 inss1 
 |-  ( ~P W i^i Fin ) C_ ~P W
24 22 23 sstrdi 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> ran f C_ ~P W )
25 sspwuni 
 |-  ( ran f C_ ~P W <-> U. ran f C_ W )
26 24 25 sylib 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U. ran f C_ W )
27 21 26 eqsstrd 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U_ z e. w ( f ` z ) C_ W )
28 vex 
 |-  w e. _V
29 fvex 
 |-  ( f ` z ) e. _V
30 28 29 iunex 
 |-  U_ z e. w ( f ` z ) e. _V
31 30 elpw 
 |-  ( U_ z e. w ( f ` z ) e. ~P W <-> U_ z e. w ( f ` z ) C_ W )
32 27 31 sylibr 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U_ z e. w ( f ` z ) e. ~P W )
33 inss2 
 |-  ( ~P S i^i Fin ) C_ Fin
34 simplr 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> w e. ( ~P S i^i Fin ) )
35 33 34 sselid 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> w e. Fin )
36 inss2 
 |-  ( ~P W i^i Fin ) C_ Fin
37 fss 
 |-  ( ( f : w --> ( ~P W i^i Fin ) /\ ( ~P W i^i Fin ) C_ Fin ) -> f : w --> Fin )
38 18 36 37 sylancl 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> f : w --> Fin )
39 ffvelcdm 
 |-  ( ( f : w --> Fin /\ z e. w ) -> ( f ` z ) e. Fin )
40 39 ralrimiva 
 |-  ( f : w --> Fin -> A. z e. w ( f ` z ) e. Fin )
41 38 40 syl 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> A. z e. w ( f ` z ) e. Fin )
42 iunfi 
 |-  ( ( w e. Fin /\ A. z e. w ( f ` z ) e. Fin ) -> U_ z e. w ( f ` z ) e. Fin )
43 35 41 42 syl2anc 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U_ z e. w ( f ` z ) e. Fin )
44 32 43 elind 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U_ z e. w ( f ` z ) e. ( ~P W i^i Fin ) )
45 simprl 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> Y = U. w )
46 uniiun 
 |-  U. w = U_ z e. w z
47 45 46 eqtrdi 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> Y = U_ z e. w z )
48 47 xpeq2d 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> ( X X. Y ) = ( X X. U_ z e. w z ) )
49 xpiundi 
 |-  ( X X. U_ z e. w z ) = U_ z e. w ( X X. z )
50 48 49 eqtrdi 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> ( X X. Y ) = U_ z e. w ( X X. z ) )
51 simprrr 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> A. u e. w ( X X. u ) C_ U. ( f ` u ) )
52 xpeq2 
 |-  ( u = z -> ( X X. u ) = ( X X. z ) )
53 fveq2 
 |-  ( u = z -> ( f ` u ) = ( f ` z ) )
54 53 unieqd 
 |-  ( u = z -> U. ( f ` u ) = U. ( f ` z ) )
55 52 54 sseq12d 
 |-  ( u = z -> ( ( X X. u ) C_ U. ( f ` u ) <-> ( X X. z ) C_ U. ( f ` z ) ) )
56 55 cbvralvw 
 |-  ( A. u e. w ( X X. u ) C_ U. ( f ` u ) <-> A. z e. w ( X X. z ) C_ U. ( f ` z ) )
57 51 56 sylib 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> A. z e. w ( X X. z ) C_ U. ( f ` z ) )
58 ss2iun 
 |-  ( A. z e. w ( X X. z ) C_ U. ( f ` z ) -> U_ z e. w ( X X. z ) C_ U_ z e. w U. ( f ` z ) )
59 57 58 syl 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U_ z e. w ( X X. z ) C_ U_ z e. w U. ( f ` z ) )
60 50 59 eqsstrd 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> ( X X. Y ) C_ U_ z e. w U. ( f ` z ) )
61 18 ffvelcdmda 
 |-  ( ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) /\ z e. w ) -> ( f ` z ) e. ( ~P W i^i Fin ) )
62 23 61 sselid 
 |-  ( ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) /\ z e. w ) -> ( f ` z ) e. ~P W )
63 elpwi 
 |-  ( ( f ` z ) e. ~P W -> ( f ` z ) C_ W )
64 uniss 
 |-  ( ( f ` z ) C_ W -> U. ( f ` z ) C_ U. W )
65 62 63 64 3syl 
 |-  ( ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) /\ z e. w ) -> U. ( f ` z ) C_ U. W )
66 6 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) /\ z e. w ) -> ( X X. Y ) = U. W )
67 65 66 sseqtrrd 
 |-  ( ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) /\ z e. w ) -> U. ( f ` z ) C_ ( X X. Y ) )
68 67 ralrimiva 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> A. z e. w U. ( f ` z ) C_ ( X X. Y ) )
69 iunss 
 |-  ( U_ z e. w U. ( f ` z ) C_ ( X X. Y ) <-> A. z e. w U. ( f ` z ) C_ ( X X. Y ) )
70 68 69 sylibr 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> U_ z e. w U. ( f ` z ) C_ ( X X. Y ) )
71 60 70 eqssd 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> ( X X. Y ) = U_ z e. w U. ( f ` z ) )
72 iuncom4 
 |-  U_ z e. w U. ( f ` z ) = U. U_ z e. w ( f ` z )
73 71 72 eqtrdi 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> ( X X. Y ) = U. U_ z e. w ( f ` z ) )
74 unieq 
 |-  ( v = U_ z e. w ( f ` z ) -> U. v = U. U_ z e. w ( f ` z ) )
75 74 rspceeqv 
 |-  ( ( U_ z e. w ( f ` z ) e. ( ~P W i^i Fin ) /\ ( X X. Y ) = U. U_ z e. w ( f ` z ) ) -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v )
76 44 73 75 syl2anc 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ ( Y = U. w /\ ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) ) -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v )
77 76 expr 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ Y = U. w ) -> ( ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v ) )
78 77 exlimdv 
 |-  ( ( ( ph /\ w e. ( ~P S i^i Fin ) ) /\ Y = U. w ) -> ( E. f ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v ) )
79 78 expimpd 
 |-  ( ( ph /\ w e. ( ~P S i^i Fin ) ) -> ( ( Y = U. w /\ E. f ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v ) )
80 79 rexlimdva 
 |-  ( ph -> ( E. w e. ( ~P S i^i Fin ) ( Y = U. w /\ E. f ( f : w --> ( ~P W i^i Fin ) /\ A. u e. w ( X X. u ) C_ U. ( f ` u ) ) ) -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v ) )
81 17 80 mpd 
 |-  ( ph -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v )