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 incom 
 |-  ( ( I \ z ) i^i z ) = ( z i^i ( I \ z ) )
106 disjdif 
 |-  ( z i^i ( I \ z ) ) = (/)
107 105 106 eqtri 
 |-  ( ( I \ z ) i^i z ) = (/)
108 107 a1i 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> ( ( I \ z ) i^i z ) = (/) )
109 simpr 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x e. ( I \ z ) )
110 simplr 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> y e. z )
111 disjne 
 |-  ( ( ( ( I \ z ) i^i z ) = (/) /\ x e. ( I \ z ) /\ y e. z ) -> x =/= y )
112 108 109 110 111 syl3anc 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x =/= y )
113 112 neneqd 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> -. x = y )
114 113 iffalsed 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x = y , C , U. J ) = U. J )
115 103 104 114 3eltr4d 
 |-  ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
116 115 ralrimiva 
 |-  ( ( ph /\ y e. z ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
117 116 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 ) )
118 117 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 ) )
119 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 ) )
120 102 118 119 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 ) )
121 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 ) ) )
122 121 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 ) ) )
123 120 122 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 ) )
124 22 ad3antrrr 
 |-  ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> I e. _V )
125 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 ) ) )
126 124 125 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 ) ) )
127 123 126 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 ) )
128 127 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 ) )
129 mptexg 
 |-  ( I e. _V -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
130 22 129 syl 
 |-  ( ph -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
131 130 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 )
132 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 ) ) )
133 131 132 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 ) ) )
134 128 133 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 ) )
135 92 134 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 ) ) )
136 135 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 ) ) =/= (/) )
137 60 136 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 ) ) =/= (/) )
138 137 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 ) ) =/= (/) )
139 57 138 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 ) ) =/= (/) )
140 28 6 33 139 cmpfiiin 
 |-  ( ph -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
141 27 140 eqnetrd 
 |-  ( ph -> ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
142 12 141 eqnetrd 
 |-  ( ph -> X_ x e. I C =/= (/) )
143 n0 
 |-  ( X_ x e. I C =/= (/) <-> E. y y e. X_ x e. I C )
144 142 143 sylib 
 |-  ( ph -> E. y y e. X_ x e. I C )
145 elixp2 
 |-  ( y e. X_ x e. I C <-> ( y e. _V /\ y Fn I /\ A. x e. I ( y ` x ) e. C ) )
146 145 simp3bi 
 |-  ( y e. X_ x e. I C -> A. x e. I ( y ` x ) e. C )
147 f1ocnv 
 |-  ( B : S -1-1-onto-> C -> `' B : C -1-1-onto-> S )
148 f1of 
 |-  ( `' B : C -1-1-onto-> S -> `' B : C --> S )
149 ffvelrn 
 |-  ( ( `' B : C --> S /\ ( y ` x ) e. C ) -> ( `' B ` ( y ` x ) ) e. S )
150 149 ex 
 |-  ( `' B : C --> S -> ( ( y ` x ) e. C -> ( `' B ` ( y ` x ) ) e. S ) )
151 4 147 148 150 4syl 
 |-  ( ( ph /\ x e. I ) -> ( ( y ` x ) e. C -> ( `' B ` ( y ` x ) ) e. S ) )
152 151 ralimdva 
 |-  ( ph -> ( A. x e. I ( y ` x ) e. C -> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
153 152 imp 
 |-  ( ( ph /\ A. x e. I ( y ` x ) e. C ) -> A. x e. I ( `' B ` ( y ` x ) ) e. S )
154 146 153 sylan2 
 |-  ( ( ph /\ y e. X_ x e. I C ) -> A. x e. I ( `' B ` ( y ` x ) ) e. S )
155 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 ) )
156 22 155 syl 
 |-  ( ph -> ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S <-> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
157 156 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 ) )
158 154 157 mpbird 
 |-  ( ( ph /\ y e. X_ x e. I C ) -> ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S )
159 158 ne0d 
 |-  ( ( ph /\ y e. X_ x e. I C ) -> X_ x e. I S =/= (/) )
160 144 159 exlimddv 
 |-  ( ph -> X_ x e. I S =/= (/) )