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