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 ffvelrn
 |-  ( ( `' 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 =/= (/) )