MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isr0 Structured version   Unicode version

Theorem isr0 20404
Description: The property " J is an R0 space". A space is R0 if any two topologically distinguishable points are separated (there is an open set containing each one and disjoint from the other). Or in contraposition, if every open set which contains  x also contains  y, so there is no separation, then  x and  y are members of the same open sets. We have chosen not to give this definition a name, because it turns out that a space is R0 if and only if its Kolmogorov quotient is T1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2  |-  F  =  ( x  e.  X  |->  { y  e.  J  |  x  e.  y } )
Assertion
Ref Expression
isr0  |-  ( J  e.  (TopOn `  X
)  ->  ( (KQ `  J )  e.  Fre  <->  A. z  e.  X  A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) ) )
Distinct variable groups:    w, o, x, y, z, J    o, F, w, z    o, X, w, x, y, z
Allowed substitution hints:    F( x, y)

Proof of Theorem isr0
Dummy variables  a 
b  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kqval.2 . . . . . . . . . . . 12  |-  F  =  ( x  e.  X  |->  { y  e.  J  |  x  e.  y } )
21kqid 20395 . . . . . . . . . . 11  |-  ( J  e.  (TopOn `  X
)  ->  F  e.  ( J  Cn  (KQ `  J ) ) )
32ad2antrr 723 . . . . . . . . . 10  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  ->  F  e.  ( J  Cn  (KQ `  J ) ) )
4 cnima 19933 . . . . . . . . . 10  |-  ( ( F  e.  ( J  Cn  (KQ `  J
) )  /\  v  e.  (KQ `  J ) )  ->  ( `' F " v )  e.  J )
53, 4sylan 469 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  ( `' F " v )  e.  J )
6 eleq2 2527 . . . . . . . . . . 11  |-  ( o  =  ( `' F " v )  ->  (
z  e.  o  <->  z  e.  ( `' F " v ) ) )
7 eleq2 2527 . . . . . . . . . . 11  |-  ( o  =  ( `' F " v )  ->  (
w  e.  o  <->  w  e.  ( `' F " v ) ) )
86, 7imbi12d 318 . . . . . . . . . 10  |-  ( o  =  ( `' F " v )  ->  (
( z  e.  o  ->  w  e.  o )  <->  ( z  e.  ( `' F "
v )  ->  w  e.  ( `' F "
v ) ) ) )
98rspcv 3203 . . . . . . . . 9  |-  ( ( `' F " v )  e.  J  ->  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  ( z  e.  ( `' F "
v )  ->  w  e.  ( `' F "
v ) ) ) )
105, 9syl 16 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  ( A. o  e.  J  (
z  e.  o  ->  w  e.  o )  ->  ( z  e.  ( `' F " v )  ->  w  e.  ( `' F " v ) ) ) )
111kqffn 20392 . . . . . . . . . . . . 13  |-  ( J  e.  (TopOn `  X
)  ->  F  Fn  X )
1211ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  ->  F  Fn  X )
1312adantr 463 . . . . . . . . . . 11  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  F  Fn  X )
14 fnfun 5660 . . . . . . . . . . 11  |-  ( F  Fn  X  ->  Fun  F )
1513, 14syl 16 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  Fun  F )
16 simprl 754 . . . . . . . . . . . 12  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
z  e.  X )
1716adantr 463 . . . . . . . . . . 11  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  z  e.  X )
18 fndm 5662 . . . . . . . . . . . 12  |-  ( F  Fn  X  ->  dom  F  =  X )
1913, 18syl 16 . . . . . . . . . . 11  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  dom  F  =  X )
2017, 19eleqtrrd 2545 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  z  e.  dom  F )
21 fvimacnv 5978 . . . . . . . . . 10  |-  ( ( Fun  F  /\  z  e.  dom  F )  -> 
( ( F `  z )  e.  v  <-> 
z  e.  ( `' F " v ) ) )
2215, 20, 21syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  ( ( F `  z )  e.  v  <->  z  e.  ( `' F " v ) ) )
23 simprr 755 . . . . . . . . . . . 12  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  ->  w  e.  X )
2423adantr 463 . . . . . . . . . . 11  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  w  e.  X )
2524, 19eleqtrrd 2545 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  w  e.  dom  F )
26 fvimacnv 5978 . . . . . . . . . 10  |-  ( ( Fun  F  /\  w  e.  dom  F )  -> 
( ( F `  w )  e.  v  <-> 
w  e.  ( `' F " v ) ) )
2715, 25, 26syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  ( ( F `  w )  e.  v  <->  w  e.  ( `' F " v ) ) )
2822, 27imbi12d 318 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  ( (
( F `  z
)  e.  v  -> 
( F `  w
)  e.  v )  <-> 
( z  e.  ( `' F " v )  ->  w  e.  ( `' F " v ) ) ) )
2910, 28sylibrd 234 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X
) )  /\  v  e.  (KQ `  J ) )  ->  ( A. o  e.  J  (
z  e.  o  ->  w  e.  o )  ->  ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v ) ) )
3029ralrimdva 2872 . . . . . 6  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v ) ) )
31 simplr 753 . . . . . . 7  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
(KQ `  J )  e.  Fre )
32 fnfvelrn 6004 . . . . . . . . 9  |-  ( ( F  Fn  X  /\  z  e.  X )  ->  ( F `  z
)  e.  ran  F
)
3312, 16, 32syl2anc 659 . . . . . . . 8  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( F `  z
)  e.  ran  F
)
341kqtopon 20394 . . . . . . . . . 10  |-  ( J  e.  (TopOn `  X
)  ->  (KQ `  J
)  e.  (TopOn `  ran  F ) )
3534ad2antrr 723 . . . . . . . . 9  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
(KQ `  J )  e.  (TopOn `  ran  F ) )
36 toponuni 19595 . . . . . . . . 9  |-  ( (KQ
`  J )  e.  (TopOn `  ran  F )  ->  ran  F  =  U. (KQ `  J ) )
3735, 36syl 16 . . . . . . . 8  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  ->  ran  F  =  U. (KQ `  J ) )
3833, 37eleqtrd 2544 . . . . . . 7  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( F `  z
)  e.  U. (KQ `  J ) )
39 fnfvelrn 6004 . . . . . . . . 9  |-  ( ( F  Fn  X  /\  w  e.  X )  ->  ( F `  w
)  e.  ran  F
)
4012, 23, 39syl2anc 659 . . . . . . . 8  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( F `  w
)  e.  ran  F
)
4140, 37eleqtrd 2544 . . . . . . 7  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( F `  w
)  e.  U. (KQ `  J ) )
42 eqid 2454 . . . . . . . 8  |-  U. (KQ `  J )  =  U. (KQ `  J )
4342t1sep2 20037 . . . . . . 7  |-  ( ( (KQ `  J )  e.  Fre  /\  ( F `  z )  e.  U. (KQ `  J
)  /\  ( F `  w )  e.  U. (KQ `  J ) )  ->  ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) )
4431, 38, 41, 43syl3anc 1226 . . . . . 6  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) )
4530, 44syld 44 . . . . 5  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  ( F `  z )  =  ( F `  w ) ) )
461kqfeq 20391 . . . . . . . 8  |-  ( ( J  e.  (TopOn `  X )  /\  z  e.  X  /\  w  e.  X )  ->  (
( F `  z
)  =  ( F `
 w )  <->  A. y  e.  J  ( z  e.  y  <->  w  e.  y
) ) )
47 eleq2 2527 . . . . . . . . . 10  |-  ( o  =  y  ->  (
z  e.  o  <->  z  e.  y ) )
48 eleq2 2527 . . . . . . . . . 10  |-  ( o  =  y  ->  (
w  e.  o  <->  w  e.  y ) )
4947, 48bibi12d 319 . . . . . . . . 9  |-  ( o  =  y  ->  (
( z  e.  o  <-> 
w  e.  o )  <-> 
( z  e.  y  <-> 
w  e.  y ) ) )
5049cbvralv 3081 . . . . . . . 8  |-  ( A. o  e.  J  (
z  e.  o  <->  w  e.  o )  <->  A. y  e.  J  ( z  e.  y  <->  w  e.  y
) )
5146, 50syl6bbr 263 . . . . . . 7  |-  ( ( J  e.  (TopOn `  X )  /\  z  e.  X  /\  w  e.  X )  ->  (
( F `  z
)  =  ( F `
 w )  <->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) )
52513expb 1195 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  (
z  e.  X  /\  w  e.  X )
)  ->  ( ( F `  z )  =  ( F `  w )  <->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) )
5352adantlr 712 . . . . 5  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( ( F `  z )  =  ( F `  w )  <->  A. o  e.  J  ( z  e.  o  <-> 
w  e.  o ) ) )
5445, 53sylibd 214 . . . 4  |-  ( ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  /\  ( z  e.  X  /\  w  e.  X ) )  -> 
( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) )
5554ralrimivva 2875 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  (KQ `  J )  e.  Fre )  ->  A. z  e.  X  A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) )
5655ex 432 . 2  |-  ( J  e.  (TopOn `  X
)  ->  ( (KQ `  J )  e.  Fre  ->  A. z  e.  X  A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) ) )
57 simpll 751 . . . . . . . . . . 11  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  J  e.  (TopOn `  X )
)
581kqopn 20401 . . . . . . . . . . 11  |-  ( ( J  e.  (TopOn `  X )  /\  o  e.  J )  ->  ( F " o )  e.  (KQ `  J ) )
5957, 58sylan 469 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X
)  /\  w  e.  X )  /\  o  e.  J )  ->  ( F " o )  e.  (KQ `  J ) )
60 eleq2 2527 . . . . . . . . . . . 12  |-  ( v  =  ( F "
o )  ->  (
( F `  z
)  e.  v  <->  ( F `  z )  e.  ( F " o ) ) )
61 eleq2 2527 . . . . . . . . . . . 12  |-  ( v  =  ( F "
o )  ->  (
( F `  w
)  e.  v  <->  ( F `  w )  e.  ( F " o ) ) )
6260, 61imbi12d 318 . . . . . . . . . . 11  |-  ( v  =  ( F "
o )  ->  (
( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  <->  ( ( F `
 z )  e.  ( F " o
)  ->  ( F `  w )  e.  ( F " o ) ) ) )
6362rspcv 3203 . . . . . . . . . 10  |-  ( ( F " o )  e.  (KQ `  J
)  ->  ( A. v  e.  (KQ `  J
) ( ( F `
 z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( ( F `  z )  e.  ( F " o
)  ->  ( F `  w )  e.  ( F " o ) ) ) )
6459, 63syl 16 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X
)  /\  w  e.  X )  /\  o  e.  J )  ->  ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  ->  (
( F `  z
)  e.  ( F
" o )  -> 
( F `  w
)  e.  ( F
" o ) ) ) )
651kqfvima 20397 . . . . . . . . . . . . 13  |-  ( ( J  e.  (TopOn `  X )  /\  o  e.  J  /\  z  e.  X )  ->  (
z  e.  o  <->  ( F `  z )  e.  ( F " o ) ) )
66653expa 1194 . . . . . . . . . . . 12  |-  ( ( ( J  e.  (TopOn `  X )  /\  o  e.  J )  /\  z  e.  X )  ->  (
z  e.  o  <->  ( F `  z )  e.  ( F " o ) ) )
6766an32s 802 . . . . . . . . . . 11  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  o  e.  J )  ->  (
z  e.  o  <->  ( F `  z )  e.  ( F " o ) ) )
6867adantlr 712 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X
)  /\  w  e.  X )  /\  o  e.  J )  ->  (
z  e.  o  <->  ( F `  z )  e.  ( F " o ) ) )
691kqfvima 20397 . . . . . . . . . . . . 13  |-  ( ( J  e.  (TopOn `  X )  /\  o  e.  J  /\  w  e.  X )  ->  (
w  e.  o  <->  ( F `  w )  e.  ( F " o ) ) )
70693expa 1194 . . . . . . . . . . . 12  |-  ( ( ( J  e.  (TopOn `  X )  /\  o  e.  J )  /\  w  e.  X )  ->  (
w  e.  o  <->  ( F `  w )  e.  ( F " o ) ) )
7170an32s 802 . . . . . . . . . . 11  |-  ( ( ( J  e.  (TopOn `  X )  /\  w  e.  X )  /\  o  e.  J )  ->  (
w  e.  o  <->  ( F `  w )  e.  ( F " o ) ) )
7271adantllr 716 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X
)  /\  w  e.  X )  /\  o  e.  J )  ->  (
w  e.  o  <->  ( F `  w )  e.  ( F " o ) ) )
7368, 72imbi12d 318 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X
)  /\  w  e.  X )  /\  o  e.  J )  ->  (
( z  e.  o  ->  w  e.  o )  <->  ( ( F `
 z )  e.  ( F " o
)  ->  ( F `  w )  e.  ( F " o ) ) ) )
7464, 73sylibrd 234 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X
)  /\  w  e.  X )  /\  o  e.  J )  ->  ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  ->  (
z  e.  o  ->  w  e.  o )
) )
7574ralrimdva 2872 . . . . . . 7  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  ->  A. o  e.  J  ( z  e.  o  ->  w  e.  o ) ) )
761kqfval 20390 . . . . . . . . . . 11  |-  ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  ->  ( F `  z )  =  { y  e.  J  |  z  e.  y } )
7776adantr 463 . . . . . . . . . 10  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  ( F `  z )  =  { y  e.  J  |  z  e.  y } )
781kqfval 20390 . . . . . . . . . . 11  |-  ( ( J  e.  (TopOn `  X )  /\  w  e.  X )  ->  ( F `  w )  =  { y  e.  J  |  w  e.  y } )
7978adantlr 712 . . . . . . . . . 10  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  ( F `  w )  =  { y  e.  J  |  w  e.  y } )
8077, 79eqeq12d 2476 . . . . . . . . 9  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  (
( F `  z
)  =  ( F `
 w )  <->  { y  e.  J  |  z  e.  y }  =  {
y  e.  J  |  w  e.  y }
) )
81 rabbi 3033 . . . . . . . . . 10  |-  ( A. y  e.  J  (
z  e.  y  <->  w  e.  y )  <->  { y  e.  J  |  z  e.  y }  =  {
y  e.  J  |  w  e.  y }
)
8250, 81bitri 249 . . . . . . . . 9  |-  ( A. o  e.  J  (
z  e.  o  <->  w  e.  o )  <->  { y  e.  J  |  z  e.  y }  =  {
y  e.  J  |  w  e.  y }
)
8380, 82syl6bbr 263 . . . . . . . 8  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  (
( F `  z
)  =  ( F `
 w )  <->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) )
8483biimprd 223 . . . . . . 7  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  ( A. o  e.  J  ( z  e.  o  <-> 
w  e.  o )  ->  ( F `  z )  =  ( F `  w ) ) )
8575, 84imim12d 74 . . . . . 6  |-  ( ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  /\  w  e.  X )  ->  (
( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) )  ->  ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
8685ralimdva 2862 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  z  e.  X )  ->  ( A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) )  ->  A. w  e.  X  ( A. v  e.  (KQ `  J
) ( ( F `
 z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
8786ralimdva 2862 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  ( A. z  e.  X  A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) )  ->  A. z  e.  X  A. w  e.  X  ( A. v  e.  (KQ `  J
) ( ( F `
 z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
88 eleq1 2526 . . . . . . . . . . 11  |-  ( a  =  ( F `  z )  ->  (
a  e.  v  <->  ( F `  z )  e.  v ) )
8988imbi1d 315 . . . . . . . . . 10  |-  ( a  =  ( F `  z )  ->  (
( a  e.  v  ->  b  e.  v )  <->  ( ( F `
 z )  e.  v  ->  b  e.  v ) ) )
9089ralbidv 2893 . . . . . . . . 9  |-  ( a  =  ( F `  z )  ->  ( A. v  e.  (KQ `  J ) ( a  e.  v  ->  b  e.  v )  <->  A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  b  e.  v ) ) )
91 eqeq1 2458 . . . . . . . . 9  |-  ( a  =  ( F `  z )  ->  (
a  =  b  <->  ( F `  z )  =  b ) )
9290, 91imbi12d 318 . . . . . . . 8  |-  ( a  =  ( F `  z )  ->  (
( A. v  e.  (KQ `  J ) ( a  e.  v  ->  b  e.  v )  ->  a  =  b )  <->  ( A. v  e.  (KQ `  J
) ( ( F `
 z )  e.  v  ->  b  e.  v )  ->  ( F `  z )  =  b ) ) )
9392ralbidv 2893 . . . . . . 7  |-  ( a  =  ( F `  z )  ->  ( A. b  e.  ran  F ( A. v  e.  (KQ `  J ) ( a  e.  v  ->  b  e.  v )  ->  a  =  b )  <->  A. b  e.  ran  F ( A. v  e.  (KQ `  J
) ( ( F `
 z )  e.  v  ->  b  e.  v )  ->  ( F `  z )  =  b ) ) )
9493ralrn 6010 . . . . . 6  |-  ( F  Fn  X  ->  ( A. a  e.  ran  F A. b  e.  ran  F ( A. v  e.  (KQ `  J ) ( a  e.  v  ->  b  e.  v )  ->  a  =  b )  <->  A. z  e.  X  A. b  e.  ran  F ( A. v  e.  (KQ `  J
) ( ( F `
 z )  e.  v  ->  b  e.  v )  ->  ( F `  z )  =  b ) ) )
95 eleq1 2526 . . . . . . . . . . 11  |-  ( b  =  ( F `  w )  ->  (
b  e.  v  <->  ( F `  w )  e.  v ) )
9695imbi2d 314 . . . . . . . . . 10  |-  ( b  =  ( F `  w )  ->  (
( ( F `  z )  e.  v  ->  b  e.  v )  <->  ( ( F `
 z )  e.  v  ->  ( F `  w )  e.  v ) ) )
9796ralbidv 2893 . . . . . . . . 9  |-  ( b  =  ( F `  w )  ->  ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  b  e.  v )  <->  A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v ) ) )
98 eqeq2 2469 . . . . . . . . 9  |-  ( b  =  ( F `  w )  ->  (
( F `  z
)  =  b  <->  ( F `  z )  =  ( F `  w ) ) )
9997, 98imbi12d 318 . . . . . . . 8  |-  ( b  =  ( F `  w )  ->  (
( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  b  e.  v )  ->  ( F `  z )  =  b )  <->  ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
10099ralrn 6010 . . . . . . 7  |-  ( F  Fn  X  ->  ( A. b  e.  ran  F ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  b  e.  v )  ->  ( F `  z )  =  b )  <->  A. w  e.  X  ( A. v  e.  (KQ
`  J ) ( ( F `  z
)  e.  v  -> 
( F `  w
)  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
101100ralbidv 2893 . . . . . 6  |-  ( F  Fn  X  ->  ( A. z  e.  X  A. b  e.  ran  F ( A. v  e.  (KQ `  J ) ( ( F `  z )  e.  v  ->  b  e.  v )  ->  ( F `  z )  =  b )  <->  A. z  e.  X  A. w  e.  X  ( A. v  e.  (KQ
`  J ) ( ( F `  z
)  e.  v  -> 
( F `  w
)  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
10294, 101bitrd 253 . . . . 5  |-  ( F  Fn  X  ->  ( A. a  e.  ran  F A. b  e.  ran  F ( A. v  e.  (KQ `  J ) ( a  e.  v  ->  b  e.  v )  ->  a  =  b )  <->  A. z  e.  X  A. w  e.  X  ( A. v  e.  (KQ `  J
) ( ( F `
 z )  e.  v  ->  ( F `  w )  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
10311, 102syl 16 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  ( A. a  e.  ran  F A. b  e.  ran  F ( A. v  e.  (KQ
`  J ) ( a  e.  v  -> 
b  e.  v )  ->  a  =  b )  <->  A. z  e.  X  A. w  e.  X  ( A. v  e.  (KQ
`  J ) ( ( F `  z
)  e.  v  -> 
( F `  w
)  e.  v )  ->  ( F `  z )  =  ( F `  w ) ) ) )
10487, 103sylibrd 234 . . 3  |-  ( J  e.  (TopOn `  X
)  ->  ( A. z  e.  X  A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) )  ->  A. a  e.  ran  F A. b  e.  ran  F ( A. v  e.  (KQ `  J
) ( a  e.  v  ->  b  e.  v )  ->  a  =  b ) ) )
105 ist1-2 20015 . . . 4  |-  ( (KQ
`  J )  e.  (TopOn `  ran  F )  ->  ( (KQ `  J )  e.  Fre  <->  A. a  e.  ran  F A. b  e.  ran  F ( A. v  e.  (KQ
`  J ) ( a  e.  v  -> 
b  e.  v )  ->  a  =  b ) ) )
10634, 105syl 16 . . 3  |-  ( J  e.  (TopOn `  X
)  ->  ( (KQ `  J )  e.  Fre  <->  A. a  e.  ran  F A. b  e.  ran  F ( A. v  e.  (KQ
`  J ) ( a  e.  v  -> 
b  e.  v )  ->  a  =  b ) ) )
107104, 106sylibrd 234 . 2  |-  ( J  e.  (TopOn `  X
)  ->  ( A. z  e.  X  A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) )  ->  (KQ `  J )  e.  Fre ) )
10856, 107impbid 191 1  |-  ( J  e.  (TopOn `  X
)  ->  ( (KQ `  J )  e.  Fre  <->  A. z  e.  X  A. w  e.  X  ( A. o  e.  J  ( z  e.  o  ->  w  e.  o )  ->  A. o  e.  J  ( z  e.  o  <->  w  e.  o
) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823   A.wral 2804   {crab 2808   U.cuni 4235    |-> cmpt 4497   `'ccnv 4987   dom cdm 4988   ran crn 4989   "cima 4991   Fun wfun 5564    Fn wfn 5565   ` cfv 5570  (class class class)co 6270  TopOnctopon 19562    Cn ccn 19892   Frect1 19975  KQckq 20360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-map 7414  df-topgen 14933  df-qtop 14996  df-top 19566  df-topon 19569  df-cld 19687  df-cn 19895  df-t1 19982  df-kq 20361
This theorem is referenced by:  r0sep  20415
  Copyright terms: Public domain W3C validator