Metamath Proof Explorer

Theorem ptcmplem4

Description: Lemma for ptcmp . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses ptcmp.1 
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
ptcmp.2 
|- X = X_ n e. A U. ( F ` n )
ptcmp.3 
|- ( ph -> A e. V )
ptcmp.4 
|- ( ph -> F : A --> Comp )
ptcmp.5 
|- ( ph -> X e. ( UFL i^i dom card ) )
ptcmplem2.5 
|- ( ph -> U C_ ran S )
ptcmplem2.6 
|- ( ph -> X = U. U )
ptcmplem2.7 
|- ( ph -> -. E. z e. ( ~P U i^i Fin ) X = U. z )
ptcmplem3.8 
|- K = { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U }
Assertion ptcmplem4 
|- -. ph

Proof

Step Hyp Ref Expression
1 ptcmp.1 
 |-  S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
2 ptcmp.2 
 |-  X = X_ n e. A U. ( F ` n )
3 ptcmp.3 
 |-  ( ph -> A e. V )
4 ptcmp.4 
 |-  ( ph -> F : A --> Comp )
5 ptcmp.5 
 |-  ( ph -> X e. ( UFL i^i dom card ) )
6 ptcmplem2.5 
 |-  ( ph -> U C_ ran S )
7 ptcmplem2.6 
 |-  ( ph -> X = U. U )
8 ptcmplem2.7 
 |-  ( ph -> -. E. z e. ( ~P U i^i Fin ) X = U. z )
9 ptcmplem3.8 
 |-  K = { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U }
10 1 2 3 4 5 6 7 8 9 ptcmplem3 
 |-  ( ph -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
11 simprl 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f Fn A )
12 eldifi 
 |-  ( ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> ( f ` k ) e. U. ( F ` k ) )
13 12 ralimi 
 |-  ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A ( f ` k ) e. U. ( F ` k ) )
14 fveq2 
 |-  ( n = k -> ( f ` n ) = ( f ` k ) )
15 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
16 15 unieqd 
 |-  ( n = k -> U. ( F ` n ) = U. ( F ` k ) )
17 14 16 eleq12d 
 |-  ( n = k -> ( ( f ` n ) e. U. ( F ` n ) <-> ( f ` k ) e. U. ( F ` k ) ) )
18 17 cbvralvw 
 |-  ( A. n e. A ( f ` n ) e. U. ( F ` n ) <-> A. k e. A ( f ` k ) e. U. ( F ` k ) )
19 13 18 sylibr 
 |-  ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. n e. A ( f ` n ) e. U. ( F ` n ) )
20 19 ad2antll 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> A. n e. A ( f ` n ) e. U. ( F ` n ) )
21 vex 
 |-  f e. _V
22 21 elixp 
 |-  ( f e. X_ n e. A U. ( F ` n ) <-> ( f Fn A /\ A. n e. A ( f ` n ) e. U. ( F ` n ) ) )
23 11 20 22 sylanbrc 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. X_ n e. A U. ( F ` n ) )
24 23 2 eleqtrrdi 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. X )
25 7 adantr 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> X = U. U )
26 24 25 eleqtrd 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. U. U )
27 eluni2 
 |-  ( f e. U. U <-> E. v e. U f e. v )
28 26 27 sylib 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> E. v e. U f e. v )
29 simplrr 
 |-  ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> f e. v )
30 29 adantr 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> f e. v )
31 simprr 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> v = ( `' ( w e. X |-> ( w ` k ) ) " u ) )
32 30 31 eleqtrd 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> f e. ( `' ( w e. X |-> ( w ` k ) ) " u ) )
33 fveq1 
 |-  ( w = f -> ( w ` k ) = ( f ` k ) )
34 33 eleq1d 
 |-  ( w = f -> ( ( w ` k ) e. u <-> ( f ` k ) e. u ) )
35 eqid 
 |-  ( w e. X |-> ( w ` k ) ) = ( w e. X |-> ( w ` k ) )
36 35 mptpreima 
 |-  ( `' ( w e. X |-> ( w ` k ) ) " u ) = { w e. X | ( w ` k ) e. u }
37 34 36 elrab2 
 |-  ( f e. ( `' ( w e. X |-> ( w ` k ) ) " u ) <-> ( f e. X /\ ( f ` k ) e. u ) )
38 37 simprbi 
 |-  ( f e. ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. u )
39 32 38 syl 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> ( f ` k ) e. u )
40 simprl 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> u e. ( F ` k ) )
41 simplrl 
 |-  ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> v e. U )
42 41 adantr 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> v e. U )
43 31 42 eqeltrrd 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U )
44 rabid 
 |-  ( u e. { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U } <-> ( u e. ( F ` k ) /\ ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U ) )
45 40 43 44 sylanbrc 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> u e. { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U } )
46 45 9 eleqtrrdi 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> u e. K )
47 elunii 
 |-  ( ( ( f ` k ) e. u /\ u e. K ) -> ( f ` k ) e. U. K )
48 39 46 47 syl2anc 
 |-  ( ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( u e. ( F ` k ) /\ v = ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> ( f ` k ) e. U. K )
49 48 rexlimdvaa 
 |-  ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ ( k e. A /\ ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) )
50 49 expr 
 |-  ( ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) /\ k e. A ) -> ( ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) )
51 50 ralimdva 
 |-  ( ( ( ph /\ f Fn A ) /\ ( v e. U /\ f e. v ) ) -> ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) )
52 51 ex 
 |-  ( ( ph /\ f Fn A ) -> ( ( v e. U /\ f e. v ) -> ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) ) )
53 52 com23 
 |-  ( ( ph /\ f Fn A ) -> ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> ( ( v e. U /\ f e. v ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) ) )
54 53 impr 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> ( ( v e. U /\ f e. v ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) ) )
55 54 imp 
 |-  ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) )
56 6 adantr 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> U C_ ran S )
57 56 sselda 
 |-  ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ v e. U ) -> v e. ran S )
58 57 adantrr 
 |-  ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> v e. ran S )
59 1 rnmpo 
 |-  ran S = { v | E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) }
60 58 59 eleqtrdi 
 |-  ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> v e. { v | E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) } )
61 abid 
 |-  ( v e. { v | E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) } <-> E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) )
62 60 61 sylib 
 |-  ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) )
63 rexim 
 |-  ( A. k e. A ( E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> ( f ` k ) e. U. K ) -> ( E. k e. A E. u e. ( F ` k ) v = ( `' ( w e. X |-> ( w ` k ) ) " u ) -> E. k e. A ( f ` k ) e. U. K ) )
64 55 62 63 sylc 
 |-  ( ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) /\ ( v e. U /\ f e. v ) ) -> E. k e. A ( f ` k ) e. U. K )
65 28 64 rexlimddv 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> E. k e. A ( f ` k ) e. U. K )
66 eldifn 
 |-  ( ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> -. ( f ` k ) e. U. K )
67 66 ralimi 
 |-  ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A -. ( f ` k ) e. U. K )
68 67 ad2antll 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> A. k e. A -. ( f ` k ) e. U. K )
69 ralnex 
 |-  ( A. k e. A -. ( f ` k ) e. U. K <-> -. E. k e. A ( f ` k ) e. U. K )
70 68 69 sylib 
 |-  ( ( ph /\ ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> -. E. k e. A ( f ` k ) e. U. K )
71 65 70 pm2.65da 
 |-  ( ph -> -. ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
72 71 nexdv 
 |-  ( ph -> -. E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
73 10 72 pm2.65i 
 |-  -. ph