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 35892
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 2422 . . . . . . . 8  |-  U. J  =  U. J
32cldss 20043 . . . . . . 7  |-  ( C  e.  ( Clsd `  J
)  ->  C  C_  U. J
)
41, 3syl 17 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  C  C_ 
U. J )
54ralrimiva 2836 . . . . 5  |-  ( ph  ->  A. x  e.  I  C  C_  U. J )
6 boxriin 7576 . . . . 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 17 . . . 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 20409 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Comp  ->  (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top )
10 0ntop 19934 . . . . . . . . . . 11  |-  -.  (/)  e.  Top
11 fvprc 5876 . . . . . . . . . . . 12  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  =  (/) )
1211eleq1d 2491 . . . . . . . . . . 11  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top  <->  (/)  e.  Top ) )
1310, 12mtbiri 304 . . . . . . . . . 10  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  -.  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top )
1413con4i 133 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top  ->  ( x  e.  I  |->  J )  e.  _V )
158, 9, 143syl 18 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J )  e.  _V )
16 kelac1.j . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  J  e.  Top )
17 eqid 2422 . . . . . . . . 9  |-  ( x  e.  I  |->  J )  =  ( x  e.  I  |->  J )
1816, 17fmptd 6062 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J ) : I --> Top )
19 dmfex 6766 . . . . . . . 8  |-  ( ( ( x  e.  I  |->  J )  e.  _V  /\  ( x  e.  I  |->  J ) : I --> Top )  ->  I  e.  _V )
2015, 18, 19syl2anc 665 . . . . . . 7  |-  ( ph  ->  I  e.  _V )
2116ralrimiva 2836 . . . . . . 7  |-  ( ph  ->  A. x  e.  I  J  e.  Top )
22 eqid 2422 . . . . . . . 8  |-  ( Xt_ `  ( x  e.  I  |->  J ) )  =  ( Xt_ `  (
x  e.  I  |->  J ) )
2322ptunimpt 20609 . . . . . . 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 665 . . . . . 6  |-  ( ph  -> 
X_ x  e.  I  U. J  =  U. ( Xt_ `  ( x  e.  I  |->  J ) ) )
2524ineq1d 3663 . . . . 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 2422 . . . . . 6  |-  U. ( Xt_ `  ( x  e.  I  |->  J ) )  =  U. ( Xt_ `  ( x  e.  I  |->  J ) )
272topcld 20049 . . . . . . . . . 10  |-  ( J  e.  Top  ->  U. J  e.  ( Clsd `  J
) )
2816, 27syl 17 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  U. J  e.  ( Clsd `  J
) )
291, 28ifcld 3954 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  if ( x  =  y ,  C ,  U. J
)  e.  ( Clsd `  J ) )
3020, 16, 29ptcldmpt 20628 . . . . . . 7  |-  ( ph  -> 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  ( Xt_ `  ( x  e.  I  |->  J ) ) ) )
3130adantr 466 . . . . . 6  |-  ( (
ph  /\  y  e.  I )  ->  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
)  e.  ( Clsd `  ( Xt_ `  (
x  e.  I  |->  J ) ) ) )
32 simprr 764 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  e.  Fin )
33 kelac1.b . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  B : S -1-1-onto-> C )
34 f1ofo 5838 . . . . . . . . . . . . . . 15  |-  ( B : S -1-1-onto-> C  ->  B : S -onto-> C )
35 foima 5815 . . . . . . . . . . . . . . 15  |-  ( B : S -onto-> C  -> 
( B " S
)  =  C )
3633, 34, 353syl 18 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =  C )
3736eqcomd 2430 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  C  =  ( B " S ) )
38 kelac1.z . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  S  =/=  (/) )
39 f1ofn 5832 . . . . . . . . . . . . . . . . 17  |-  ( B : S -1-1-onto-> C  ->  B  Fn  S )
4033, 39syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  B  Fn  S )
41 ssid 3483 . . . . . . . . . . . . . . . 16  |-  S  C_  S
42 fnimaeq0 5715 . . . . . . . . . . . . . . . 16  |-  ( ( B  Fn  S  /\  S  C_  S )  -> 
( ( B " S )  =  (/)  <->  S  =  (/) ) )
4340, 41, 42sylancl 666 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =  (/)  <->  S  =  (/) ) )
4443necon3bid 2678 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =/=  (/)  <->  S  =/=  (/) ) )
4538, 44mpbird 235 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =/=  (/) )
4637, 45eqnetrd 2713 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  I )  ->  C  =/=  (/) )
47 n0 3771 . . . . . . . . . . . 12  |-  ( C  =/=  (/)  <->  E. w  w  e.  C )
4846, 47sylib 199 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  E. w  w  e.  C )
49 rexv 3096 . . . . . . . . . . 11  |-  ( E. w  e.  _V  w  e.  C  <->  E. w  w  e.  C )
5048, 49sylibr 215 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  I )  ->  E. w  e.  _V  w  e.  C
)
5150ralrimiva 2836 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  I  E. w  e.  _V  w  e.  C )
52 ssralv 3525 . . . . . . . . . 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 ) )
5352adantr 466 . . . . . . . . 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 )
)
5451, 53mpan9 471 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  A. x  e.  z  E. w  e.  _V  w  e.  C )
55 eleq1 2495 . . . . . . . . 9  |-  ( w  =  ( f `  x )  ->  (
w  e.  C  <->  ( f `  x )  e.  C
) )
5655ac6sfi 7825 . . . . . . . 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
) )
5732, 54, 56syl2anc 665 . . . . . . 7  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  E. f ( f : z --> _V  /\  A. x  e.  z  ( f `  x )  e.  C
) )
5824eqcomd 2430 . . . . . . . . . . 11  |-  ( ph  ->  U. ( Xt_ `  (
x  e.  I  |->  J ) )  =  X_ x  e.  I  U. J )
5958ineq1d 3663 . . . . . . . . . 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 ) ) )
6059ad2antrr 730 . . . . . . . . 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
) ) )
61 iftrue 3917 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  z  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  ( f `
 x ) )
6261ad2antrl 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 758 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  ph )
64 simprl 762 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  C_  I )
6564sselda 3464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  x  e.  I )
6663, 65, 4syl2anc 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  C  C_ 
U. J )
6766sseld 3463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  -> 
( f `  x
)  e.  U. J
) )
6867impr 623 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  U. J
)
6962, 68eqeltrd 2507 . . . . . . . . . . . . . . . . 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
)
7069expr 618 . . . . . . . . . . . . . . . 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
) )
7170ralimdva 2830 . . . . . . . . . . . . . . 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 ) )
7271imp 430 . . . . . . . . . . . . . 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 )
73 eldifn 3588 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( I  \ 
z )  ->  -.  x  e.  z )
7473iffalsed 3922 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
7574adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
76 eldifi 3587 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  x  e.  I )
77 kelac1.u . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  U  e.  U. J )
7876, 77sylan2 476 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
7975, 78eqeltrd 2507 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
)
8079ralrimiva 2836 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  ( I  \  z ) if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  U. J )
8180ad2antrr 730 . . . . . . . . . . . . . 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 )
82 ralun 3648 . . . . . . . . . . . . . 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 )
8372, 81, 82syl2anc 665 . . . . . . . . . . . . 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 )
84 undif 3878 . . . . . . . . . . . . . . . . 17  |-  ( z 
C_  I  <->  ( z  u.  ( I  \  z
) )  =  I )
8584biimpi 197 . . . . . . . . . . . . . . . 16  |-  ( z 
C_  I  ->  (
z  u.  ( I 
\  z ) )  =  I )
8685ad2antrl 732 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( z  u.  (
I  \  z )
)  =  I )
8786raleqdv 3028 . . . . . . . . . . . . . 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 ) )
8887adantr 466 . . . . . . . . . . . . 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 ) )
8983, 88mpbid 213 . . . . . . . . . . . 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 )
9020ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  I  e.  _V )
91 mptelixpg 7571 . . . . . . . . . . . . 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
) )
9290, 91syl 17 . . . . . . . . . . . 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
) )
9389, 92mpbird 235 . . . . . . . . . . 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 )
94 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C  =  if ( x  =  y ,  C ,  U. J )  -> 
( ( f `  x )  e.  C  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J ) ) )
95 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. J  =  if (
x  =  y ,  C ,  U. J
)  ->  ( (
f `  x )  e.  U. J  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J
) ) )
96 simplrr 769 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  x  =  y )  ->  (
f `  x )  e.  C )
9768adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  -.  x  =  y )  -> 
( f `  x
)  e.  U. J
)
9894, 95, 96, 97ifbothda 3946 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  if ( x  =  y ,  C ,  U. J
) )
9962, 98eqeltrd 2507 . . . . . . . . . . . . . . . . . . . 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
) )
10099expr 618 . . . . . . . . . . . . . . . . . . 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
) ) )
101100ralimdva 2830 . . . . . . . . . . . . . . . . . 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
) ) )
102101imp 430 . . . . . . . . . . . . . . . . 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 ) )
103102adantr 466 . . . . . . . . . . . . . . . 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 ) )
10478adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
10574adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
106 incom 3655 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( I  \  z )  i^i  z )  =  ( z  i^i  (
I  \  z )
)
107 disjdif 3869 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  i^i  ( I  \ 
z ) )  =  (/)
108106, 107eqtri 2451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( I  \  z )  i^i  z )  =  (/)
109108a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  (
( I  \  z
)  i^i  z )  =  (/) )
110 simpr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  e.  ( I  \  z
) )
111 simplr 760 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  y  e.  z )
112 disjne 3840 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( I  \ 
z )  i^i  z
)  =  (/)  /\  x  e.  ( I  \  z
)  /\  y  e.  z )  ->  x  =/=  y )
113109, 110, 111, 112syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  =/=  y )
114113neneqd 2621 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  -.  x  =  y )
115114iffalsed 3922 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  =  y ,  C ,  U. J
)  =  U. J
)
116104, 105, 1153eltr4d 2522 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  if ( x  =  y ,  C ,  U. J
) )
117116ralrimiva 2836 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  z )  ->  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
118117adantlr 719 . . . . . . . . . . . . . . . . 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 ) )
119118adantlr 719 . . . . . . . . . . . . . . . 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 ) )
120 ralun 3648 . . . . . . . . . . . . . . . 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
) )
121103, 119, 120syl2anc 665 . . . . . . . . . . . . . . 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 ) )
12286raleqdv 3028 . . . . . . . . . . . . . . . 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 ) ) )
123122ad2antrr 730 . . . . . . . . . . . . . . 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
) ) )
124121, 123mpbid 213 . . . . . . . . . . . . . 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 ) )
12520ad3antrrr 734 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  I  e.  _V )
126 mptelixpg 7571 . . . . . . . . . . . . . . 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 ) ) )
127125, 126syl 17 . . . . . . . . . . . . . 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 ) ) )
128124, 127mpbird 235 . . . . . . . . . . . . 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
) )
129128ralrimiva 2836 . . . . . . . . . . . 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
) )
130 mptexg 6151 . . . . . . . . . . . . . . 15  |-  ( I  e.  _V  ->  (
x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  _V )
13120, 130syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  I  |->  if ( x  e.  z ,  ( f `
 x ) ,  U ) )  e. 
_V )
132131ad2antrr 730 . . . . . . . . . . . . 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 )
133 eliin 4305 . . . . . . . . . . . . 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
) ) )
134132, 133syl 17 . . . . . . . . . . . 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 ) ) )
135129, 134mpbird 235 . . . . . . . . . . 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 ) )
13693, 135elind 3650 . . . . . . . . . 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 ) ) )
137 ne0i 3767 . . . . . . . . . 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
) )  =/=  (/) )
138136, 137syl 17 . . . . . . . . 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 ) )  =/=  (/) )
13960, 138eqnetrd 2713 . . . . . . . 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 ) )  =/=  (/) )
140139adantrl 720 . . . . . . 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 ) )  =/=  (/) )
14157, 140exlimddv 1774 . . . . . 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
) )  =/=  (/) )
14226, 8, 31, 141cmpfiiin 35509 . . . . 5  |-  ( ph  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
14325, 142eqnetrd 2713 . . . 4  |-  ( ph  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
1447, 143eqnetrd 2713 . . 3  |-  ( ph  -> 
X_ x  e.  I  C  =/=  (/) )
145 n0 3771 . . 3  |-  ( X_ x  e.  I  C  =/=  (/)  <->  E. y  y  e.  X_ x  e.  I  C )
146144, 145sylib 199 . 2  |-  ( ph  ->  E. y  y  e.  X_ x  e.  I  C )
147 elixp2 7538 . . . . . 6  |-  ( y  e.  X_ x  e.  I  C 
<->  ( y  e.  _V  /\  y  Fn  I  /\  A. x  e.  I  ( y `  x )  e.  C ) )
148147simp3bi 1022 . . . . 5  |-  ( y  e.  X_ x  e.  I  C  ->  A. x  e.  I 
( y `  x
)  e.  C )
149 f1ocnv 5843 . . . . . . . 8  |-  ( B : S -1-1-onto-> C  ->  `' B : C -1-1-onto-> S )
150 f1of 5831 . . . . . . . 8  |-  ( `' B : C -1-1-onto-> S  ->  `' B : C --> S )
151 ffvelrn 6036 . . . . . . . . 9  |-  ( ( `' B : C --> S  /\  ( y `  x
)  e.  C )  ->  ( `' B `  ( y `  x
) )  e.  S
)
152151ex 435 . . . . . . . 8  |-  ( `' B : C --> S  -> 
( ( y `  x )  e.  C  ->  ( `' B `  ( y `  x
) )  e.  S
) )
15333, 149, 150, 1524syl 19 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  (
( y `  x
)  e.  C  -> 
( `' B `  ( y `  x
) )  e.  S
) )
154153ralimdva 2830 . . . . . 6  |-  ( ph  ->  ( A. x  e.  I  ( y `  x )  e.  C  ->  A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
155154imp 430 . . . . 5  |-  ( (
ph  /\  A. x  e.  I  ( y `  x )  e.  C
)  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
156148, 155sylan2 476 . . . 4  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
157 mptelixpg 7571 . . . . . 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
) )
15820, 157syl 17 . . . . 5  |-  ( ph  ->  ( ( x  e.  I  |->  ( `' B `  ( y `  x
) ) )  e.  X_ x  e.  I  S 
<-> 
A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
159158adantr 466 . . . 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 ) )
160156, 159mpbird 235 . . 3  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S )
161 ne0i 3767 . . 3  |-  ( ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S  ->  X_ x  e.  I  S  =/=  (/) )
162160, 161syl 17 . 2  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  X_ x  e.  I  S  =/=  (/) )
163146, 162exlimddv 1774 1  |-  ( ph  -> 
X_ x  e.  I  S  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2614   A.wral 2771   E.wrex 2772   _Vcvv 3080    \ cdif 3433    u. cun 3434    i^i cin 3435    C_ wss 3436   (/)c0 3761   ifcif 3911   U.cuni 4219   |^|_ciin 4300    |-> cmpt 4482   `'ccnv 4852   "cima 4856    Fn wfn 5596   -->wf 5597   -onto->wfo 5599   -1-1-onto->wf1o 5600   ` cfv 5601   X_cixp 7534   Fincfn 7581   Xt_cpt 15337   Topctop 19916   Clsdccld 20030   Compccmp 20400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-iin 4302  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-2o 7195  df-oadd 7198  df-er 7375  df-map 7486  df-ixp 7535  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-fi 7935  df-topgen 15342  df-pt 15343  df-top 19920  df-bases 19921  df-cld 20033  df-cmp 20401
This theorem is referenced by:  kelac2  35894
  Copyright terms: Public domain W3C validator