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 ffvelrnda
 |-  ( ( 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 syl5bir
 |-  ( ( 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 syl5bi
 |-  ( ( 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 ) ) )