Metamath Proof Explorer

Theorem ptcmplem3

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 ptcmplem3 
|- ( ph -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )

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 rabexg 
 |-  ( A e. V -> { n e. A | -. U. ( F ` n ) ~~ 1o } e. _V )
11 3 10 syl 
 |-  ( ph -> { n e. A | -. U. ( F ` n ) ~~ 1o } e. _V )
12 1 2 3 4 5 6 7 8 ptcmplem2 
 |-  ( ph -> U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } U. ( F ` k ) e. dom card )
13 eldifi 
 |-  ( y e. ( U. ( F ` k ) \ U. K ) -> y e. U. ( F ` k ) )
14 13 3ad2ant3 
 |-  ( ( ph /\ y e. _V /\ y e. ( U. ( F ` k ) \ U. K ) ) -> y e. U. ( F ` k ) )
15 14 rabssdv 
 |-  ( ph -> { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } C_ U. ( F ` k ) )
16 15 ralrimivw 
 |-  ( ph -> A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } C_ U. ( F ` k ) )
17 ss2iun 
 |-  ( A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } C_ U. ( F ` k ) -> U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } C_ U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } U. ( F ` k ) )
18 16 17 syl 
 |-  ( ph -> U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } C_ U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } U. ( F ` k ) )
19 ssnum 
 |-  ( ( U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } U. ( F ` k ) e. dom card /\ U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } C_ U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } U. ( F ` k ) ) -> U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } e. dom card )
20 12 18 19 syl2anc 
 |-  ( ph -> U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } e. dom card )
21 elrabi 
 |-  ( k e. { n e. A | -. U. ( F ` n ) ~~ 1o } -> k e. A )
22 8 adantr 
 |-  ( ( ph /\ k e. A ) -> -. E. z e. ( ~P U i^i Fin ) X = U. z )
23 ssdif0 
 |-  ( U. ( F ` k ) C_ U. K <-> ( U. ( F ` k ) \ U. K ) = (/) )
24 4 ffvelcdmda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. Comp )
25 24 adantr 
 |-  ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) -> ( F ` k ) e. Comp )
26 9 ssrab3 
 |-  K C_ ( F ` k )
27 26 a1i 
 |-  ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) -> K C_ ( F ` k ) )
28 simpr 
 |-  ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) -> U. ( F ` k ) C_ U. K )
29 uniss 
 |-  ( K C_ ( F ` k ) -> U. K C_ U. ( F ` k ) )
30 26 29 mp1i 
 |-  ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) -> U. K C_ U. ( F ` k ) )
31 28 30 eqssd 
 |-  ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) -> U. ( F ` k ) = U. K )
32 eqid 
 |-  U. ( F ` k ) = U. ( F ` k )
33 32 cmpcov 
 |-  ( ( ( F ` k ) e. Comp /\ K C_ ( F ` k ) /\ U. ( F ` k ) = U. K ) -> E. t e. ( ~P K i^i Fin ) U. ( F ` k ) = U. t )
34 25 27 31 33 syl3anc 
 |-  ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) -> E. t e. ( ~P K i^i Fin ) U. ( F ` k ) = U. t )
35 elfpw 
 |-  ( t e. ( ~P K i^i Fin ) <-> ( t C_ K /\ t e. Fin ) )
36 35 simplbi 
 |-  ( t e. ( ~P K i^i Fin ) -> t C_ K )
37 36 ad2antrl 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> t C_ K )
38 37 sselda 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ x e. t ) -> x e. K )
39 imaeq2 
 |-  ( u = x -> ( `' ( w e. X |-> ( w ` k ) ) " u ) = ( `' ( w e. X |-> ( w ` k ) ) " x ) )
40 39 eleq1d 
 |-  ( u = x -> ( ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U <-> ( `' ( w e. X |-> ( w ` k ) ) " x ) e. U ) )
41 40 9 elrab2 
 |-  ( x e. K <-> ( x e. ( F ` k ) /\ ( `' ( w e. X |-> ( w ` k ) ) " x ) e. U ) )
42 41 simprbi 
 |-  ( x e. K -> ( `' ( w e. X |-> ( w ` k ) ) " x ) e. U )
43 38 42 syl 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ x e. t ) -> ( `' ( w e. X |-> ( w ` k ) ) " x ) e. U )
44 43 fmpttd 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) : t --> U )
45 44 frnd 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) C_ U )
46 35 simprbi 
 |-  ( t e. ( ~P K i^i Fin ) -> t e. Fin )
47 46 ad2antrl 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> t e. Fin )
48 eqid 
 |-  ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) = ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) )
49 48 rnmpt 
 |-  ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) = { f | E. x e. t f = ( `' ( w e. X |-> ( w ` k ) ) " x ) }
50 abrexfi 
 |-  ( t e. Fin -> { f | E. x e. t f = ( `' ( w e. X |-> ( w ` k ) ) " x ) } e. Fin )
51 49 50 eqeltrid 
 |-  ( t e. Fin -> ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) e. Fin )
52 47 51 syl 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) e. Fin )
53 elfpw 
 |-  ( ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) e. ( ~P U i^i Fin ) <-> ( ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) C_ U /\ ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) e. Fin ) )
54 45 52 53 sylanbrc 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) e. ( ~P U i^i Fin ) )
55 fveq2 
 |-  ( n = k -> ( f ` n ) = ( f ` k ) )
56 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
57 56 unieqd 
 |-  ( n = k -> U. ( F ` n ) = U. ( F ` k ) )
58 55 57 eleq12d 
 |-  ( n = k -> ( ( f ` n ) e. U. ( F ` n ) <-> ( f ` k ) e. U. ( F ` k ) ) )
59 simpr 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> f e. X )
60 59 2 eleqtrdi 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> f e. X_ n e. A U. ( F ` n ) )
61 vex 
 |-  f e. _V
62 61 elixp 
 |-  ( f e. X_ n e. A U. ( F ` n ) <-> ( f Fn A /\ A. n e. A ( f ` n ) e. U. ( F ` n ) ) )
63 62 simprbi 
 |-  ( f e. X_ n e. A U. ( F ` n ) -> A. n e. A ( f ` n ) e. U. ( F ` n ) )
64 60 63 syl 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> A. n e. A ( f ` n ) e. U. ( F ` n ) )
65 simp-4r 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> k e. A )
66 58 64 65 rspcdva 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> ( f ` k ) e. U. ( F ` k ) )
67 simplrr 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> U. ( F ` k ) = U. t )
68 66 67 eleqtrd 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> ( f ` k ) e. U. t )
69 eluni2 
 |-  ( ( f ` k ) e. U. t <-> E. x e. t ( f ` k ) e. x )
70 68 69 sylib 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> E. x e. t ( f ` k ) e. x )
71 fveq1 
 |-  ( w = f -> ( w ` k ) = ( f ` k ) )
72 71 eleq1d 
 |-  ( w = f -> ( ( w ` k ) e. x <-> ( f ` k ) e. x ) )
73 eqid 
 |-  ( w e. X |-> ( w ` k ) ) = ( w e. X |-> ( w ` k ) )
74 73 mptpreima 
 |-  ( `' ( w e. X |-> ( w ` k ) ) " x ) = { w e. X | ( w ` k ) e. x }
75 72 74 elrab2 
 |-  ( f e. ( `' ( w e. X |-> ( w ` k ) ) " x ) <-> ( f e. X /\ ( f ` k ) e. x ) )
76 75 baib 
 |-  ( f e. X -> ( f e. ( `' ( w e. X |-> ( w ` k ) ) " x ) <-> ( f ` k ) e. x ) )
77 76 ad2antlr 
 |-  ( ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) /\ x e. t ) -> ( f e. ( `' ( w e. X |-> ( w ` k ) ) " x ) <-> ( f ` k ) e. x ) )
78 77 rexbidva 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> ( E. x e. t f e. ( `' ( w e. X |-> ( w ` k ) ) " x ) <-> E. x e. t ( f ` k ) e. x ) )
79 70 78 mpbird 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> E. x e. t f e. ( `' ( w e. X |-> ( w ` k ) ) " x ) )
80 eliun 
 |-  ( f e. U_ x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) <-> E. x e. t f e. ( `' ( w e. X |-> ( w ` k ) ) " x ) )
81 79 80 sylibr 
 |-  ( ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) /\ f e. X ) -> f e. U_ x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) )
82 81 ex 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> ( f e. X -> f e. U_ x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) ) )
83 82 ssrdv 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> X C_ U_ x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) )
84 43 ralrimiva 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> A. x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) e. U )
85 dfiun2g 
 |-  ( A. x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) e. U -> U_ x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) = U. { f | E. x e. t f = ( `' ( w e. X |-> ( w ` k ) ) " x ) } )
86 84 85 syl 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> U_ x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) = U. { f | E. x e. t f = ( `' ( w e. X |-> ( w ` k ) ) " x ) } )
87 49 unieqi 
 |-  U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) = U. { f | E. x e. t f = ( `' ( w e. X |-> ( w ` k ) ) " x ) }
88 86 87 eqtr4di 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> U_ x e. t ( `' ( w e. X |-> ( w ` k ) ) " x ) = U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) )
89 83 88 sseqtrd 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> X C_ U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) )
90 45 unissd 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) C_ U. U )
91 7 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> X = U. U )
92 90 91 sseqtrrd 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) C_ X )
93 89 92 eqssd 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> X = U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) )
94 unieq 
 |-  ( z = ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) -> U. z = U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) )
95 94 rspceeqv 
 |-  ( ( ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) e. ( ~P U i^i Fin ) /\ X = U. ran ( x e. t |-> ( `' ( w e. X |-> ( w ` k ) ) " x ) ) ) -> E. z e. ( ~P U i^i Fin ) X = U. z )
96 54 93 95 syl2anc 
 |-  ( ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) /\ ( t e. ( ~P K i^i Fin ) /\ U. ( F ` k ) = U. t ) ) -> E. z e. ( ~P U i^i Fin ) X = U. z )
97 34 96 rexlimddv 
 |-  ( ( ( ph /\ k e. A ) /\ U. ( F ` k ) C_ U. K ) -> E. z e. ( ~P U i^i Fin ) X = U. z )
98 97 ex 
 |-  ( ( ph /\ k e. A ) -> ( U. ( F ` k ) C_ U. K -> E. z e. ( ~P U i^i Fin ) X = U. z ) )
99 23 98 biimtrrid 
 |-  ( ( ph /\ k e. A ) -> ( ( U. ( F ` k ) \ U. K ) = (/) -> E. z e. ( ~P U i^i Fin ) X = U. z ) )
100 22 99 mtod 
 |-  ( ( ph /\ k e. A ) -> -. ( U. ( F ` k ) \ U. K ) = (/) )
101 neq0 
 |-  ( -. ( U. ( F ` k ) \ U. K ) = (/) <-> E. y y e. ( U. ( F ` k ) \ U. K ) )
102 100 101 sylib 
 |-  ( ( ph /\ k e. A ) -> E. y y e. ( U. ( F ` k ) \ U. K ) )
103 rexv 
 |-  ( E. y e. _V y e. ( U. ( F ` k ) \ U. K ) <-> E. y y e. ( U. ( F ` k ) \ U. K ) )
104 102 103 sylibr 
 |-  ( ( ph /\ k e. A ) -> E. y e. _V y e. ( U. ( F ` k ) \ U. K ) )
105 21 104 sylan2 
 |-  ( ( ph /\ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ) -> E. y e. _V y e. ( U. ( F ` k ) \ U. K ) )
106 105 ralrimiva 
 |-  ( ph -> A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } E. y e. _V y e. ( U. ( F ` k ) \ U. K ) )
107 eleq1 
 |-  ( y = ( g ` k ) -> ( y e. ( U. ( F ` k ) \ U. K ) <-> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
108 107 ac6num 
 |-  ( ( { n e. A | -. U. ( F ` n ) ~~ 1o } e. _V /\ U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } { y e. _V | y e. ( U. ( F ` k ) \ U. K ) } e. dom card /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } E. y e. _V y e. ( U. ( F ` k ) \ U. K ) ) -> E. g ( g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
109 11 20 106 108 syl3anc 
 |-  ( ph -> E. g ( g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
110 3 adantr 
 |-  ( ( ph /\ ( g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> A e. V )
111 110 mptexd 
 |-  ( ( ph /\ ( g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) e. _V )
112 fvex 
 |-  ( F ` m ) e. _V
113 112 uniex 
 |-  U. ( F ` m ) e. _V
114 113 uniex 
 |-  U. U. ( F ` m ) e. _V
115 fvex 
 |-  ( g ` m ) e. _V
116 114 115 ifex 
 |-  if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) e. _V
117 116 rgenw 
 |-  A. m e. A if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) e. _V
118 eqid 
 |-  ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) = ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) )
119 118 fnmpt 
 |-  ( A. m e. A if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) e. _V -> ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) Fn A )
120 117 119 mp1i 
 |-  ( ( ph /\ ( g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) Fn A )
121 57 breq1d 
 |-  ( n = k -> ( U. ( F ` n ) ~~ 1o <-> U. ( F ` k ) ~~ 1o ) )
122 121 notbid 
 |-  ( n = k -> ( -. U. ( F ` n ) ~~ 1o <-> -. U. ( F ` k ) ~~ 1o ) )
123 122 ralrab 
 |-  ( A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) <-> A. k e. A ( -. U. ( F ` k ) ~~ 1o -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
124 iftrue 
 |-  ( U. ( F ` k ) ~~ 1o -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) = U. U. ( F ` k ) )
125 124 ad2antll 
 |-  ( ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) = U. U. ( F ` k ) )
126 102 adantrr 
 |-  ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) -> E. y y e. ( U. ( F ` k ) \ U. K ) )
127 13 adantl 
 |-  ( ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) /\ y e. ( U. ( F ` k ) \ U. K ) ) -> y e. U. ( F ` k ) )
128 simplrr 
 |-  ( ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) /\ y e. ( U. ( F ` k ) \ U. K ) ) -> U. ( F ` k ) ~~ 1o )
129 en1b 
 |-  ( U. ( F ` k ) ~~ 1o <-> U. ( F ` k ) = { U. U. ( F ` k ) } )
130 128 129 sylib 
 |-  ( ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) /\ y e. ( U. ( F ` k ) \ U. K ) ) -> U. ( F ` k ) = { U. U. ( F ` k ) } )
131 127 130 eleqtrd 
 |-  ( ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) /\ y e. ( U. ( F ` k ) \ U. K ) ) -> y e. { U. U. ( F ` k ) } )
132 elsni 
 |-  ( y e. { U. U. ( F ` k ) } -> y = U. U. ( F ` k ) )
133 131 132 syl 
 |-  ( ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) /\ y e. ( U. ( F ` k ) \ U. K ) ) -> y = U. U. ( F ` k ) )
134 simpr 
 |-  ( ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) /\ y e. ( U. ( F ` k ) \ U. K ) ) -> y e. ( U. ( F ` k ) \ U. K ) )
135 133 134 eqeltrrd 
 |-  ( ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) /\ y e. ( U. ( F ` k ) \ U. K ) ) -> U. U. ( F ` k ) e. ( U. ( F ` k ) \ U. K ) )
136 126 135 exlimddv 
 |-  ( ( ph /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) -> U. U. ( F ` k ) e. ( U. ( F ` k ) \ U. K ) )
137 136 adantlr 
 |-  ( ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) -> U. U. ( F ` k ) e. ( U. ( F ` k ) \ U. K ) )
138 125 137 eqeltrd 
 |-  ( ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) )
139 138 a1d 
 |-  ( ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) /\ ( k e. A /\ U. ( F ` k ) ~~ 1o ) ) -> ( ( -. U. ( F ` k ) ~~ 1o -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) )
140 139 expr 
 |-  ( ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) /\ k e. A ) -> ( U. ( F ` k ) ~~ 1o -> ( ( -. U. ( F ` k ) ~~ 1o -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) ) )
141 pm2.27 
 |-  ( -. U. ( F ` k ) ~~ 1o -> ( ( -. U. ( F ` k ) ~~ 1o -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
142 iffalse 
 |-  ( -. U. ( F ` k ) ~~ 1o -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) = ( g ` k ) )
143 142 eleq1d 
 |-  ( -. U. ( F ` k ) ~~ 1o -> ( if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) <-> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
144 141 143 sylibrd 
 |-  ( -. U. ( F ` k ) ~~ 1o -> ( ( -. U. ( F ` k ) ~~ 1o -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) )
145 140 144 pm2.61d1 
 |-  ( ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) /\ k e. A ) -> ( ( -. U. ( F ` k ) ~~ 1o -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) -> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) )
146 145 ralimdva 
 |-  ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) -> ( A. k e. A ( -. U. ( F ` k ) ~~ 1o -> ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) -> A. k e. A if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) )
147 123 146 biimtrid 
 |-  ( ( ph /\ g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V ) -> ( A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) -> A. k e. A if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) )
148 147 impr 
 |-  ( ( ph /\ ( g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> A. k e. A if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) )
149 fneq1 
 |-  ( f = ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) -> ( f Fn A <-> ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) Fn A ) )
150 fveq1 
 |-  ( f = ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) -> ( f ` k ) = ( ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) ` k ) )
151 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
152 151 unieqd 
 |-  ( m = k -> U. ( F ` m ) = U. ( F ` k ) )
153 152 breq1d 
 |-  ( m = k -> ( U. ( F ` m ) ~~ 1o <-> U. ( F ` k ) ~~ 1o ) )
154 152 unieqd 
 |-  ( m = k -> U. U. ( F ` m ) = U. U. ( F ` k ) )
155 fveq2 
 |-  ( m = k -> ( g ` m ) = ( g ` k ) )
156 153 154 155 ifbieq12d 
 |-  ( m = k -> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) = if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) )
157 fvex 
 |-  ( F ` k ) e. _V
158 157 uniex 
 |-  U. ( F ` k ) e. _V
159 158 uniex 
 |-  U. U. ( F ` k ) e. _V
160 fvex 
 |-  ( g ` k ) e. _V
161 159 160 ifex 
 |-  if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. _V
162 156 118 161 fvmpt 
 |-  ( k e. A -> ( ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) ` k ) = if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) )
163 150 162 sylan9eq 
 |-  ( ( f = ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) /\ k e. A ) -> ( f ` k ) = if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) )
164 163 eleq1d 
 |-  ( ( f = ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) /\ k e. A ) -> ( ( f ` k ) e. ( U. ( F ` k ) \ U. K ) <-> if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) )
165 164 ralbidva 
 |-  ( f = ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) -> ( A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) <-> A. k e. A if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) )
166 149 165 anbi12d 
 |-  ( f = ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) -> ( ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) <-> ( ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) Fn A /\ A. k e. A if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) ) )
167 166 spcegv 
 |-  ( ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) e. _V -> ( ( ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) Fn A /\ A. k e. A if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) )
168 167 3impib 
 |-  ( ( ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) e. _V /\ ( m e. A |-> if ( U. ( F ` m ) ~~ 1o , U. U. ( F ` m ) , ( g ` m ) ) ) Fn A /\ A. k e. A if ( U. ( F ` k ) ~~ 1o , U. U. ( F ` k ) , ( g ` k ) ) e. ( U. ( F ` k ) \ U. K ) ) -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
169 111 120 148 168 syl3anc 
 |-  ( ( ph /\ ( g : { n e. A | -. U. ( F ` n ) ~~ 1o } --> _V /\ A. k e. { n e. A | -. U. ( F ` n ) ~~ 1o } ( g ` k ) e. ( U. ( F ` k ) \ U. K ) ) ) -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
170 109 169 exlimddv 
 |-  ( ph -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )