Metamath Proof Explorer

Theorem kelac1

Description: Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypotheses kelac1.z 
|- ( ( ph /\ x e. I ) -> S =/= (/) )
kelac1.j 
|- ( ( ph /\ x e. I ) -> J e. Top )
kelac1.c 
|- ( ( ph /\ x e. I ) -> C e. ( Clsd ` J ) )
kelac1.b 
|- ( ( ph /\ x e. I ) -> B : S -1-1-onto-> C )
kelac1.u 
|- ( ( ph /\ x e. I ) -> U e. U. J )
kelac1.k 
|- ( ph -> ( Xt_ ` ( x e. I |-> J ) ) e. Comp )
Assertion kelac1 
|- ( ph -> X_ x e. I S =/= (/) )

Proof

Step Hyp Ref Expression
1 kelac1.z 
 |-  ( ( ph /\ x e. I ) -> S =/= (/) )
2 kelac1.j 
 |-  ( ( ph /\ x e. I ) -> J e. Top )
3 kelac1.c 
 |-  ( ( ph /\ x e. I ) -> C e. ( Clsd ` J ) )
4 kelac1.b 
 |-  ( ( ph /\ x e. I ) -> B : S -1-1-onto-> C )
5 kelac1.u 
 |-  ( ( ph /\ x e. I ) -> U e. U. J )
6 kelac1.k 
 |-  ( ph -> ( Xt_ ` ( x e. I |-> J ) ) e. Comp )
7 eqid 
 |-  U. J = U. J
8 7 cldss 
 |-  ( C e. ( Clsd ` J ) -> C C_ U. J )
9 3 8 syl 
 |-  ( ( ph /\ x e. I ) -> C C_ U. J )
10 9 ralrimiva 
 |-  ( ph -> A. x e. I C C_ U. J )
11 boxriin 
 |-  ( A. x e. I C C_ U. J -> X_ x e. I C = ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) )
12 10 11 syl 
 |-  ( ph -> X_ x e. I C = ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) )
13 cmptop 
 |-  ( ( Xt_ ` ( x e. I |-> J ) ) e. Comp -> ( Xt_ ` ( x e. I |-> J ) ) e. Top )
14 0ntop 
 |-  -. (/) e. Top
15 fvprc 
 |-  ( -. ( x e. I |-> J ) e. _V -> ( Xt_ ` ( x e. I |-> J ) ) = (/) )
16 15 eleq1d 
 |-  ( -. ( x e. I |-> J ) e. _V -> ( ( Xt_ ` ( x e. I |-> J ) ) e. Top <-> (/) e. Top ) )
17 14 16 mtbiri 
 |-  ( -. ( x e. I |-> J ) e. _V -> -. ( Xt_ ` ( x e. I |-> J ) ) e. Top )
18 17 con4i 
 |-  ( ( Xt_ ` ( x e. I |-> J ) ) e. Top -> ( x e. I |-> J ) e. _V )
19 6 13 18 3syl 
 |-  ( ph -> ( x e. I |-> J ) e. _V )
20 2 fmpttd 
 |-  ( ph -> ( x e. I |-> J ) : I --> Top )
21 dmfex 
 |-  ( ( ( x e. I |-> J ) e. _V /\ ( x e. I |-> J ) : I --> Top ) -> I e. _V )
22 19 20 21 syl2anc 
 |-  ( ph -> I e. _V )
23 2 ralrimiva 
 |-  ( ph -> A. x e. I J e. Top )
24 eqid 
 |-  ( Xt_ ` ( x e. I |-> J ) ) = ( Xt_ ` ( x e. I |-> J ) )
25 24 ptunimpt 
 |-  ( ( I e. _V /\ A. x e. I J e. Top ) -> X_ x e. I U. J = U. ( Xt_ ` ( x e. I |-> J ) ) )
26 22 23 25 syl2anc 
 |-  ( ph -> X_ x e. I U. J = U. ( Xt_ ` ( x e. I |-> J ) ) )
27 26 ineq1d 
 |-  ( ph -> ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) = ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) )
28 eqid 
 |-  U. ( Xt_ ` ( x e. I |-> J ) ) = U. ( Xt_ ` ( x e. I |-> J ) )
29 7 topcld 
 |-  ( J e. Top -> U. J e. ( Clsd ` J ) )
30 2 29 syl 
 |-  ( ( ph /\ x e. I ) -> U. J e. ( Clsd ` J ) )
31 3 30 ifcld 
 |-  ( ( ph /\ x e. I ) -> if ( x = y , C , U. J ) e. ( Clsd ` J ) )
32 22 2 31 ptcldmpt 
 |-  ( ph -> X_ x e. I if ( x = y , C , U. J ) e. ( Clsd ` ( Xt_ ` ( x e. I |-> J ) ) ) )
33 32 adantr 
 |-  ( ( ph /\ y e. I ) -> X_ x e. I if ( x = y , C , U. J ) e. ( Clsd ` ( Xt_ ` ( x e. I |-> J ) ) ) )
34 simprr 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> z e. Fin )
35 f1ofo 
 |-  ( B : S -1-1-onto-> C -> B : S -onto-> C )
36 foima 
 |-  ( B : S -onto-> C -> ( B " S ) = C )
37 4 35 36 3syl 
 |-  ( ( ph /\ x e. I ) -> ( B " S ) = C )
38 37 eqcomd 
 |-  ( ( ph /\ x e. I ) -> C = ( B " S ) )
39 f1ofn 
 |-  ( B : S -1-1-onto-> C -> B Fn S )
40 4 39 syl 
 |-  ( ( ph /\ x e. I ) -> B Fn S )
41 ssid 
 |-  S C_ S
42 fnimaeq0 
 |-  ( ( B Fn S /\ S C_ S ) -> ( ( B " S ) = (/) <-> S = (/) ) )
43 40 41 42 sylancl 
 |-  ( ( ph /\ x e. I ) -> ( ( B " S ) = (/) <-> S = (/) ) )
44 43 necon3bid 
 |-  ( ( ph /\ x e. I ) -> ( ( B " S ) =/= (/) <-> S =/= (/) ) )
45 1 44 mpbird 
 |-  ( ( ph /\ x e. I ) -> ( B " S ) =/= (/) )
46 38 45 eqnetrd 
 |-  ( ( ph /\ x e. I ) -> C =/= (/) )
47 n0 
 |-  ( C =/= (/) <-> E. w w e. C )
48 46 47 sylib 
 |-  ( ( ph /\ x e. I ) -> E. w w e. C )
49 rexv 
 |-  ( E. w e. _V w e. C <-> E. w w e. C )
50 48 49 sylibr 
 |-  ( ( ph /\ x e. I ) -> E. w e. _V w e. C )
51 50 ralrimiva 
 |-  ( ph -> A. x e. I E. w e. _V w e. C )
52 ssralv 
 |-  ( z C_ I -> ( A. x e. I E. w e. _V w e. C -> A. x e. z E. w e. _V w e. C ) )
53 52 adantr 
 |-  ( ( z C_ I /\ z e. Fin ) -> ( A. x e. I E. w e. _V w e. C -> A. x e. z E. w e. _V w e. C ) )
54 51 53 mpan9 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> A. x e. z E. w e. _V w e. C )
55 eleq1 
 |-  ( w = ( f ` x ) -> ( w e. C <-> ( f ` x ) e. C ) )
56 55 ac6sfi 
 |-  ( ( z e. Fin /\ A. x e. z E. w e. _V w e. C ) -> E. f ( f : z --> _V /\ A. x e. z ( f ` x ) e. C ) )
57 34 54 56 syl2anc 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> E. f ( f : z --> _V /\ A. x e. z ( f ` x ) e. C ) )
58 26 eqcomd 
 |-  ( ph -> U. ( Xt_ ` ( x e. I |-> J ) ) = X_ x e. I U. J )
59 58 ineq1d 
 |-  ( ph -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) = ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) )
60 59 ad2antrr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) = ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) )
61 iftrue 
 |-  ( x e. z -> if ( x e. z , ( f ` x ) , U ) = ( f ` x ) )
62 61 ad2antrl 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> if ( x e. z , ( f ` x ) , U ) = ( f ` x ) )
63 simpll 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ph )
64 simprl 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> z C_ I )
65 64 sselda 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> x e. I )
66 63 65 9 syl2anc 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> C C_ U. J )
67 66 sseld 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ( ( f ` x ) e. C -> ( f ` x ) e. U. J ) )
68 67 impr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> ( f ` x ) e. U. J )
69 62 68 eqeltrd 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> if ( x e. z , ( f ` x ) , U ) e. U. J )
70 69 expr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ( ( f ` x ) e. C -> if ( x e. z , ( f ` x ) , U ) e. U. J ) )
71 70 ralimdva 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. z ( f ` x ) e. C -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. U. J ) )
72 71 imp 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. U. J )
73 eldifn 
 |-  ( x e. ( I \ z ) -> -. x e. z )
74 73 iffalsed 
 |-  ( x e. ( I \ z ) -> if ( x e. z , ( f ` x ) , U ) = U )
75 74 adantl 
 |-  ( ( ph /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) = U )
76 eldifi 
 |-  ( x e. ( I \ z ) -> x e. I )
77 76 5 sylan2 
 |-  ( ( ph /\ x e. ( I \ z ) ) -> U e. U. J )
78 75 77 eqeltrd 
 |-  ( ( ph /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) e. U. J )
79 78 ralrimiva 
 |-  ( ph -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. U. J )
80 79 ad2antrr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. U. J )
81 ralun 
 |-  ( ( A. x e. z if ( x e. z , ( f ` x ) , U ) e. U. J /\ A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. U. J ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J )
82 72 80 81 syl2anc 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J )
83 undif 
 |-  ( z C_ I <-> ( z u. ( I \ z ) ) = I )
84 83 biimpi 
 |-  ( z C_ I -> ( z u. ( I \ z ) ) = I )
85 84 ad2antrl 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( z u. ( I \ z ) ) = I )
86 85 raleqdv 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
87 86 adantr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
88 82 87 mpbid 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J )
89 22 ad2antrr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> I e. _V )
90 mptelixpg 
 |-  ( I e. _V -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
91 89 90 syl 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
92 88 91 mpbird 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I U. J )
93 eleq2 
 |-  ( C = if ( x = y , C , U. J ) -> ( ( f ` x ) e. C <-> ( f ` x ) e. if ( x = y , C , U. J ) ) )
94 eleq2 
 |-  ( U. J = if ( x = y , C , U. J ) -> ( ( f ` x ) e. U. J <-> ( f ` x ) e. if ( x = y , C , U. J ) ) )
95 simplrr 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) /\ x = y ) -> ( f ` x ) e. C )
96 68 adantr 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) /\ -. x = y ) -> ( f ` x ) e. U. J )
97 93 94 95 96 ifbothda 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> ( f ` x ) e. if ( x = y , C , U. J ) )
98 62 97 eqeltrd 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
99 98 expr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ( ( f ` x ) e. C -> if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
100 99 ralimdva 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. z ( f ` x ) e. C -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
101 100 imp 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
102 101 adantr 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
103 77 adantlr 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> U e. U. J )
104 74 adantl 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) = U )
105 disjdifr 
 |-  ( ( I \ z ) i^i z ) = (/)
106 105 a1i 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> ( ( I \ z ) i^i z ) = (/) )
107 simpr 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x e. ( I \ z ) )
108 simplr 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> y e. z )
109 disjne 
 |-  ( ( ( ( I \ z ) i^i z ) = (/) /\ x e. ( I \ z ) /\ y e. z ) -> x =/= y )
110 106 107 108 109 syl3anc 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x =/= y )
111 110 neneqd 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> -. x = y )
112 111 iffalsed 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x = y , C , U. J ) = U. J )
113 103 104 112 3eltr4d 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
114 113 ralrimiva 
 |-  ( ( ph /\ y e. z ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
115 114 adantlr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ y e. z ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
116 115 adantlr 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
117 ralun 
 |-  ( ( A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) /\ A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
118 102 116 117 syl2anc 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
119 85 raleqdv 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
120 119 ad2antrr 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
121 118 120 mpbid 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
122 22 ad3antrrr 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> I e. _V )
123 mptelixpg 
 |-  ( I e. _V -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
124 122 123 syl 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
125 121 124 mpbird 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) )
126 125 ralrimiva 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. y e. z ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) )
127 mptexg 
 |-  ( I e. _V -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
128 22 127 syl 
 |-  ( ph -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
129 128 ad2antrr 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
130 eliin 
 |-  ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) <-> A. y e. z ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) ) )
131 129 130 syl 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) <-> A. y e. z ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) ) )
132 126 131 mpbird 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) )
133 92 132 elind 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) )
134 133 ne0d 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
135 60 134 eqnetrd 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
136 135 adantrl 
 |-  ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( f : z --> _V /\ A. x e. z ( f ` x ) e. C ) ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
137 57 136 exlimddv 
 |-  ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
138 28 6 33 137 cmpfiiin 
 |-  ( ph -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
139 27 138 eqnetrd 
 |-  ( ph -> ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
140 12 139 eqnetrd 
 |-  ( ph -> X_ x e. I C =/= (/) )
141 n0 
 |-  ( X_ x e. I C =/= (/) <-> E. y y e. X_ x e. I C )
142 140 141 sylib 
 |-  ( ph -> E. y y e. X_ x e. I C )
143 elixp2 
 |-  ( y e. X_ x e. I C <-> ( y e. _V /\ y Fn I /\ A. x e. I ( y ` x ) e. C ) )
144 143 simp3bi 
 |-  ( y e. X_ x e. I C -> A. x e. I ( y ` x ) e. C )
145 f1ocnv 
 |-  ( B : S -1-1-onto-> C -> `' B : C -1-1-onto-> S )
146 f1of 
 |-  ( `' B : C -1-1-onto-> S -> `' B : C --> S )
147 ffvelcdm 
 |-  ( ( `' B : C --> S /\ ( y ` x ) e. C ) -> ( `' B ` ( y ` x ) ) e. S )
148 147 ex 
 |-  ( `' B : C --> S -> ( ( y ` x ) e. C -> ( `' B ` ( y ` x ) ) e. S ) )
149 4 145 146 148 4syl 
 |-  ( ( ph /\ x e. I ) -> ( ( y ` x ) e. C -> ( `' B ` ( y ` x ) ) e. S ) )
150 149 ralimdva 
 |-  ( ph -> ( A. x e. I ( y ` x ) e. C -> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
151 150 imp 
 |-  ( ( ph /\ A. x e. I ( y ` x ) e. C ) -> A. x e. I ( `' B ` ( y ` x ) ) e. S )
152 144 151 sylan2 
 |-  ( ( ph /\ y e. X_ x e. I C ) -> A. x e. I ( `' B ` ( y ` x ) ) e. S )
153 mptelixpg 
 |-  ( I e. _V -> ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S <-> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
154 22 153 syl 
 |-  ( ph -> ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S <-> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
155 154 adantr 
 |-  ( ( ph /\ y e. X_ x e. I C ) -> ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S <-> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
156 152 155 mpbird 
 |-  ( ( ph /\ y e. X_ x e. I C ) -> ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S )
157 156 ne0d 
 |-  ( ( ph /\ y e. X_ x e. I C ) -> X_ x e. I S =/= (/) )
158 142 157 exlimddv 
 |-  ( ph -> X_ x e. I S =/= (/) )