Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  kelac1 Structured version   Unicode version

Theorem kelac1 29563
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.)
Hypotheses
Ref Expression
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
Ref Expression
kelac1  |-  ( ph  -> 
X_ x  e.  I  S  =/=  (/) )
Distinct variable groups:    ph, x    x, I
Allowed substitution hints:    B( x)    C( x)    S( x)    U( x)    J( x)

Proof of Theorem kelac1
Dummy variables  f 
y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kelac1.c . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  C  e.  ( Clsd `  J
) )
2 eqid 2454 . . . . . . . 8  |-  U. J  =  U. J
32cldss 18764 . . . . . . 7  |-  ( C  e.  ( Clsd `  J
)  ->  C  C_  U. J
)
41, 3syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  C  C_ 
U. J )
54ralrimiva 2829 . . . . 5  |-  ( ph  ->  A. x  e.  I  C  C_  U. J )
6 boxriin 7414 . . . . 5  |-  ( 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 ) ) )
75, 6syl 16 . . . 4  |-  ( 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 ) ) )
8 kelac1.k . . . . . . . . 9  |-  ( ph  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Comp )
9 cmptop 19129 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Comp  ->  (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top )
10 0ntop 18649 . . . . . . . . . . 11  |-  -.  (/)  e.  Top
11 fvprc 5792 . . . . . . . . . . . 12  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  =  (/) )
1211eleq1d 2523 . . . . . . . . . . 11  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top  <->  (/)  e.  Top ) )
1310, 12mtbiri 303 . . . . . . . . . 10  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  -.  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top )
1413con4i 130 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top  ->  ( x  e.  I  |->  J )  e.  _V )
158, 9, 143syl 20 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J )  e.  _V )
16 kelac1.j . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  J  e.  Top )
17 eqid 2454 . . . . . . . . 9  |-  ( x  e.  I  |->  J )  =  ( x  e.  I  |->  J )
1816, 17fmptd 5975 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J ) : I --> Top )
19 dmfex 6644 . . . . . . . 8  |-  ( ( ( x  e.  I  |->  J )  e.  _V  /\  ( x  e.  I  |->  J ) : I --> Top )  ->  I  e.  _V )
2015, 18, 19syl2anc 661 . . . . . . 7  |-  ( ph  ->  I  e.  _V )
2116ralrimiva 2829 . . . . . . 7  |-  ( ph  ->  A. x  e.  I  J  e.  Top )
22 eqid 2454 . . . . . . . 8  |-  ( Xt_ `  ( x  e.  I  |->  J ) )  =  ( Xt_ `  (
x  e.  I  |->  J ) )
2322ptunimpt 19299 . . . . . . 7  |-  ( ( I  e.  _V  /\  A. x  e.  I  J  e.  Top )  ->  X_ x  e.  I  U. J  =  U. ( Xt_ `  ( x  e.  I  |->  J ) ) )
2420, 21, 23syl2anc 661 . . . . . 6  |-  ( ph  -> 
X_ x  e.  I  U. J  =  U. ( Xt_ `  ( x  e.  I  |->  J ) ) )
2524ineq1d 3658 . . . . 5  |-  ( 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
) ) )
26 eqid 2454 . . . . . 6  |-  U. ( Xt_ `  ( x  e.  I  |->  J ) )  =  U. ( Xt_ `  ( x  e.  I  |->  J ) )
272topcld 18770 . . . . . . . . . 10  |-  ( J  e.  Top  ->  U. J  e.  ( Clsd `  J
) )
2816, 27syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  U. J  e.  ( Clsd `  J
) )
29 ifcl 3938 . . . . . . . . 9  |-  ( ( C  e.  ( Clsd `  J )  /\  U. J  e.  ( Clsd `  J ) )  ->  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  J )
)
301, 28, 29syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  if ( x  =  y ,  C ,  U. J
)  e.  ( Clsd `  J ) )
3120, 16, 30ptcldmpt 19318 . . . . . . 7  |-  ( ph  -> 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  ( Xt_ `  ( x  e.  I  |->  J ) ) ) )
3231adantr 465 . . . . . 6  |-  ( (
ph  /\  y  e.  I )  ->  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
)  e.  ( Clsd `  ( Xt_ `  (
x  e.  I  |->  J ) ) ) )
33 simprr 756 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  e.  Fin )
34 kelac1.b . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  B : S -1-1-onto-> C )
35 f1ofo 5755 . . . . . . . . . . . . . . 15  |-  ( B : S -1-1-onto-> C  ->  B : S -onto-> C )
36 foima 5732 . . . . . . . . . . . . . . 15  |-  ( B : S -onto-> C  -> 
( B " S
)  =  C )
3734, 35, 363syl 20 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =  C )
3837eqcomd 2462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  C  =  ( B " S ) )
39 kelac1.z . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  S  =/=  (/) )
40 f1ofn 5749 . . . . . . . . . . . . . . . . 17  |-  ( B : S -1-1-onto-> C  ->  B  Fn  S )
4134, 40syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  B  Fn  S )
42 ssid 3482 . . . . . . . . . . . . . . . 16  |-  S  C_  S
43 fnimaeq0 5639 . . . . . . . . . . . . . . . 16  |-  ( ( B  Fn  S  /\  S  C_  S )  -> 
( ( B " S )  =  (/)  <->  S  =  (/) ) )
4441, 42, 43sylancl 662 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =  (/)  <->  S  =  (/) ) )
4544necon3bid 2709 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =/=  (/)  <->  S  =/=  (/) ) )
4639, 45mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =/=  (/) )
4738, 46eqnetrd 2744 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  I )  ->  C  =/=  (/) )
48 n0 3753 . . . . . . . . . . . 12  |-  ( C  =/=  (/)  <->  E. w  w  e.  C )
4947, 48sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  E. w  w  e.  C )
50 rexv 3091 . . . . . . . . . . 11  |-  ( E. w  e.  _V  w  e.  C  <->  E. w  w  e.  C )
5149, 50sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  I )  ->  E. w  e.  _V  w  e.  C
)
5251ralrimiva 2829 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  I  E. w  e.  _V  w  e.  C )
53 ssralv 3523 . . . . . . . . . 10  |-  ( 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 ) )
5453adantr 465 . . . . . . . . 9  |-  ( ( 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 )
)
5552, 54mpan9 469 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  A. x  e.  z  E. w  e.  _V  w  e.  C )
56 eleq1 2526 . . . . . . . . 9  |-  ( w  =  ( f `  x )  ->  (
w  e.  C  <->  ( f `  x )  e.  C
) )
5756ac6sfi 7666 . . . . . . . 8  |-  ( ( 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
) )
5833, 55, 57syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  E. f ( f : z --> _V  /\  A. x  e.  z  ( f `  x )  e.  C
) )
5924eqcomd 2462 . . . . . . . . . . 11  |-  ( ph  ->  U. ( Xt_ `  (
x  e.  I  |->  J ) )  =  X_ x  e.  I  U. J )
6059ineq1d 3658 . . . . . . . . . 10  |-  ( 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 ) ) )
6160ad2antrr 725 . . . . . . . . 9  |-  ( ( ( 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
) ) )
62 iftrue 3904 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  z  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  ( f `
 x ) )
6362ad2antrl 727 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  ( f `
 x ) )
64 simpll 753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  ph )
65 simprl 755 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  C_  I )
6665sselda 3463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  x  e.  I )
6764, 66, 4syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  C  C_ 
U. J )
6867sseld 3462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  -> 
( f `  x
)  e.  U. J
) )
6968impr 619 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  U. J
)
7063, 69eqeltrd 2542 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
)
7170expr 615 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
) )
7271ralimdva 2831 . . . . . . . . . . . . . . 15  |-  ( (
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 ) )
7372imp 429 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
74 eldifn 3586 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( I  \ 
z )  ->  -.  x  e.  z )
75 iffalse 3906 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  x  e.  z  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
7674, 75syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
7776adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
78 eldifi 3585 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  x  e.  I )
79 kelac1.u . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  U  e.  U. J )
8078, 79sylan2 474 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
8177, 80eqeltrd 2542 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
)
8281ralrimiva 2829 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  ( I  \  z ) if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  U. J )
8382ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
84 ralun 3645 . . . . . . . . . . . . . 14  |-  ( ( 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 )
8573, 83, 84syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
86 undif 3866 . . . . . . . . . . . . . . . . 17  |-  ( z 
C_  I  <->  ( z  u.  ( I  \  z
) )  =  I )
8786biimpi 194 . . . . . . . . . . . . . . . 16  |-  ( z 
C_  I  ->  (
z  u.  ( I 
\  z ) )  =  I )
8887ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( z  u.  (
I  \  z )
)  =  I )
8988raleqdv 3027 . . . . . . . . . . . . . 14  |-  ( (
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 ) )
9089adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
9185, 90mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( 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 )
9220ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  I  e.  _V )
93 mptelixpg 7409 . . . . . . . . . . . . 13  |-  ( 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
) )
9492, 93syl 16 . . . . . . . . . . . 12  |-  ( ( ( 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
) )
9591, 94mpbird 232 . . . . . . . . . . 11  |-  ( ( ( 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 )
96 eleq2 2527 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C  =  if ( x  =  y ,  C ,  U. J )  -> 
( ( f `  x )  e.  C  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J ) ) )
97 eleq2 2527 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. J  =  if (
x  =  y ,  C ,  U. J
)  ->  ( (
f `  x )  e.  U. J  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J
) ) )
98 simplrr 760 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  x  =  y )  ->  (
f `  x )  e.  C )
9969adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  -.  x  =  y )  -> 
( f `  x
)  e.  U. J
)
10096, 97, 98, 99ifbothda 3931 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  if ( x  =  y ,  C ,  U. J
) )
10163, 100eqeltrd 2542 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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
) )
102101expr 615 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) ) )
103102ralimdva 2831 . . . . . . . . . . . . . . . . . 18  |-  ( (
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
) ) )
104103imp 429 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
105104adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
10680adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
10776adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
108 incom 3650 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( I  \  z )  i^i  z )  =  ( z  i^i  (
I  \  z )
)
109 disjdif 3858 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  i^i  ( I  \ 
z ) )  =  (/)
110108, 109eqtri 2483 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( I  \  z )  i^i  z )  =  (/)
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  (
( I  \  z
)  i^i  z )  =  (/) )
112 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  e.  ( I  \  z
) )
113 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  y  e.  z )
114 disjne 3831 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( I  \ 
z )  i^i  z
)  =  (/)  /\  x  e.  ( I  \  z
)  /\  y  e.  z )  ->  x  =/=  y )
115111, 112, 113, 114syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  =/=  y )
116115neneqd 2654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  -.  x  =  y )
117 iffalse 3906 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  x  =  y  ->  if ( x  =  y ,  C ,  U. J )  =  U. J )
118116, 117syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  =  y ,  C ,  U. J
)  =  U. J
)
119106, 107, 1183eltr4d 2557 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  if ( x  =  y ,  C ,  U. J
) )
120119ralrimiva 2829 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  z )  ->  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
121120adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
122121adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
123 ralun 3645 . . . . . . . . . . . . . . . 16  |-  ( ( 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
) )
124105, 122, 123syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
12588raleqdv 3027 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) ) )
126125ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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
) ) )
127124, 126mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) )
12820ad3antrrr 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  I  e.  _V )
129 mptelixpg 7409 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) )
130128, 129syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )
131127, 130mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) )
132131ralrimiva 2829 . . . . . . . . . . . 12  |-  ( ( ( 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
) )
133 mptexg 6055 . . . . . . . . . . . . . . 15  |-  ( I  e.  _V  ->  (
x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  _V )
13420, 133syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  I  |->  if ( x  e.  z ,  ( f `
 x ) ,  U ) )  e. 
_V )
135134ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
136 eliin 4283 . . . . . . . . . . . . 13  |-  ( ( 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
) ) )
137135, 136syl 16 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
138132, 137mpbird 232 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
13995, 138elind 3647 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
140 ne0i 3750 . . . . . . . . . 10  |-  ( ( 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 ) )  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
141139, 140syl 16 . . . . . . . . 9  |-  ( ( ( 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 ) )  =/=  (/) )
14261, 141eqnetrd 2744 . . . . . . . 8  |-  ( ( ( 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 ) )  =/=  (/) )
143142adantrl 715 . . . . . . 7  |-  ( ( ( 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 ) )  =/=  (/) )
14458, 143exlimddv 1693 . . . . . 6  |-  ( (
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
) )  =/=  (/) )
14526, 8, 32, 144cmpfiiin 29180 . . . . 5  |-  ( ph  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
14625, 145eqnetrd 2744 . . . 4  |-  ( ph  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
1477, 146eqnetrd 2744 . . 3  |-  ( ph  -> 
X_ x  e.  I  C  =/=  (/) )
148 n0 3753 . . 3  |-  ( X_ x  e.  I  C  =/=  (/)  <->  E. y  y  e.  X_ x  e.  I  C )
149147, 148sylib 196 . 2  |-  ( ph  ->  E. y  y  e.  X_ x  e.  I  C )
150 elixp2 7376 . . . . . 6  |-  ( y  e.  X_ x  e.  I  C 
<->  ( y  e.  _V  /\  y  Fn  I  /\  A. x  e.  I  ( y `  x )  e.  C ) )
151150simp3bi 1005 . . . . 5  |-  ( y  e.  X_ x  e.  I  C  ->  A. x  e.  I 
( y `  x
)  e.  C )
152 f1ocnv 5760 . . . . . . . 8  |-  ( B : S -1-1-onto-> C  ->  `' B : C -1-1-onto-> S )
153 f1of 5748 . . . . . . . 8  |-  ( `' B : C -1-1-onto-> S  ->  `' B : C --> S )
154 ffvelrn 5949 . . . . . . . . 9  |-  ( ( `' B : C --> S  /\  ( y `  x
)  e.  C )  ->  ( `' B `  ( y `  x
) )  e.  S
)
155154ex 434 . . . . . . . 8  |-  ( `' B : C --> S  -> 
( ( y `  x )  e.  C  ->  ( `' B `  ( y `  x
) )  e.  S
) )
15634, 152, 153, 1554syl 21 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  (
( y `  x
)  e.  C  -> 
( `' B `  ( y `  x
) )  e.  S
) )
157156ralimdva 2831 . . . . . 6  |-  ( ph  ->  ( A. x  e.  I  ( y `  x )  e.  C  ->  A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
158157imp 429 . . . . 5  |-  ( (
ph  /\  A. x  e.  I  ( y `  x )  e.  C
)  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
159151, 158sylan2 474 . . . 4  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
160 mptelixpg 7409 . . . . . 6  |-  ( I  e.  _V  ->  (
( x  e.  I  |->  ( `' B `  ( y `  x
) ) )  e.  X_ x  e.  I  S 
<-> 
A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
16120, 160syl 16 . . . . 5  |-  ( ph  ->  ( ( x  e.  I  |->  ( `' B `  ( y `  x
) ) )  e.  X_ x  e.  I  S 
<-> 
A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
162161adantr 465 . . . 4  |-  ( (
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 ) )
163159, 162mpbird 232 . . 3  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S )
164 ne0i 3750 . . 3  |-  ( ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S  ->  X_ x  e.  I  S  =/=  (/) )
165163, 164syl 16 . 2  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  X_ x  e.  I  S  =/=  (/) )
166149, 165exlimddv 1693 1  |-  ( ph  -> 
X_ x  e.  I  S  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370   E.wex 1587    e. wcel 1758    =/= wne 2647   A.wral 2798   E.wrex 2799   _Vcvv 3076    \ cdif 3432    u. cun 3433    i^i cin 3434    C_ wss 3435   (/)c0 3744   ifcif 3898   U.cuni 4198   |^|_ciin 4279    |-> cmpt 4457   `'ccnv 4946   "cima 4950    Fn wfn 5520   -->wf 5521   -onto->wfo 5523   -1-1-onto->wf1o 5524   ` cfv 5525   X_cixp 7372   Fincfn 7419   Xt_cpt 14495   Topctop 18629   Clsdccld 18751   Compccmp 19120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-iin 4281  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-om 6586  df-1st 6686  df-2nd 6687  df-recs 6941  df-rdg 6975  df-1o 7029  df-2o 7030  df-oadd 7033  df-er 7210  df-map 7325  df-ixp 7373  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-fi 7771  df-topgen 14500  df-pt 14501  df-top 18634  df-bases 18636  df-cld 18754  df-cmp 19121
This theorem is referenced by:  kelac2  29565
  Copyright terms: Public domain W3C validator