Metamath Proof Explorer

Theorem isr0

Description: The property " J is an R_0 space". A space is R_0 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 R_0 if and only if its Kolmogorov quotient is T_1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 1 kqid 
 |-  ( J e. ( TopOn ` X ) -> F e. ( J Cn ( KQ ` J ) ) )
3 2 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> F e. ( J Cn ( KQ ` J ) ) )
4 cnima 
 |-  ( ( F e. ( J Cn ( KQ ` J ) ) /\ v e. ( KQ ` J ) ) -> ( `' F " v ) e. J )
5 3 4 sylan 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> ( `' F " v ) e. J )
6 eleq2 
 |-  ( o = ( `' F " v ) -> ( z e. o <-> z e. ( `' F " v ) ) )
7 eleq2 
 |-  ( o = ( `' F " v ) -> ( w e. o <-> w e. ( `' F " v ) ) )
8 6 7 imbi12d 
 |-  ( o = ( `' F " v ) -> ( ( z e. o -> w e. o ) <-> ( z e. ( `' F " v ) -> w e. ( `' F " v ) ) ) )
9 8 rspcv 
 |-  ( ( `' F " v ) e. J -> ( A. o e. J ( z e. o -> w e. o ) -> ( z e. ( `' F " v ) -> w e. ( `' F " v ) ) ) )
10 5 9 syl 
 |-  ( ( ( ( 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 ) ) ) )
11 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
12 11 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> F Fn X )
13 12 adantr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> F Fn X )
14 fnfun 
 |-  ( F Fn X -> Fun F )
15 13 14 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> Fun F )
16 simprl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> z e. X )
17 16 adantr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> z e. X )
18 13 fndmd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> dom F = X )
19 17 18 eleqtrrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> z e. dom F )
20 fvimacnv 
 |-  ( ( Fun F /\ z e. dom F ) -> ( ( F ` z ) e. v <-> z e. ( `' F " v ) ) )
21 15 19 20 syl2anc 
 |-  ( ( ( ( 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 ) ) )
22 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> w e. X )
23 22 adantr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> w e. X )
24 23 18 eleqtrrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> w e. dom F )
25 fvimacnv 
 |-  ( ( Fun F /\ w e. dom F ) -> ( ( F ` w ) e. v <-> w e. ( `' F " v ) ) )
26 15 24 25 syl2anc 
 |-  ( ( ( ( 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 ) ) )
27 21 26 imbi12d 
 |-  ( ( ( ( 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 ) ) ) )
28 10 27 sylibrd 
 |-  ( ( ( ( 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 ) ) )
29 28 ralrimdva 
 |-  ( ( ( 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 ) ) )
30 simplr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( KQ ` J ) e. Fre )
31 fnfvelrn 
 |-  ( ( F Fn X /\ z e. X ) -> ( F ` z ) e. ran F )
32 12 16 31 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) e. ran F )
33 1 kqtopon 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
34 33 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
35 toponuni 
 |-  ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ran F = U. ( KQ ` J ) )
36 34 35 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ran F = U. ( KQ ` J ) )
37 32 36 eleqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) e. U. ( KQ ` J ) )
38 fnfvelrn 
 |-  ( ( F Fn X /\ w e. X ) -> ( F ` w ) e. ran F )
39 12 22 38 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` w ) e. ran F )
40 39 36 eleqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` w ) e. U. ( KQ ` J ) )
41 eqid 
 |-  U. ( KQ ` J ) = U. ( KQ ` J )
42 41 t1sep2 
 |-  ( ( ( 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 ) ) )
43 30 37 40 42 syl3anc 
 |-  ( ( ( 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 ) ) )
44 29 43 syld 
 |-  ( ( ( 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 ) ) )
45 1 kqfeq 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. y e. J ( z e. y <-> w e. y ) ) )
46 eleq2 
 |-  ( o = y -> ( z e. o <-> z e. y ) )
47 eleq2 
 |-  ( o = y -> ( w e. o <-> w e. y ) )
48 46 47 bibi12d 
 |-  ( o = y -> ( ( z e. o <-> w e. o ) <-> ( z e. y <-> w e. y ) ) )
49 48 cbvralvw 
 |-  ( A. o e. J ( z e. o <-> w e. o ) <-> A. y e. J ( z e. y <-> w e. y ) )
50 45 49 bitr4di 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. o e. J ( z e. o <-> w e. o ) ) )
51 50 3expb 
 |-  ( ( J e. ( TopOn ` X ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) = ( F ` w ) <-> A. o e. J ( z e. o <-> w e. o ) ) )
52 51 adantlr 
 |-  ( ( ( 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 ) ) )
53 44 52 sylibd 
 |-  ( ( ( 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 ) ) )
54 53 ralrimivva 
 |-  ( ( 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 ) ) )
55 54 ex 
 |-  ( 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 ) ) ) )
56 1 kqopn 
 |-  ( ( J e. ( TopOn ` X ) /\ o e. J ) -> ( F " o ) e. ( KQ ` J ) )
57 56 ad4ant14 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( F " o ) e. ( KQ ` J ) )
58 eleq2 
 |-  ( v = ( F " o ) -> ( ( F ` z ) e. v <-> ( F ` z ) e. ( F " o ) ) )
59 eleq2 
 |-  ( v = ( F " o ) -> ( ( F ` w ) e. v <-> ( F ` w ) e. ( F " o ) ) )
60 58 59 imbi12d 
 |-  ( v = ( F " o ) -> ( ( ( F ` z ) e. v -> ( F ` w ) e. v ) <-> ( ( F ` z ) e. ( F " o ) -> ( F ` w ) e. ( F " o ) ) ) )
61 60 rspcv 
 |-  ( ( 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 ) ) ) )
62 57 61 syl 
 |-  ( ( ( ( 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 ) ) ) )
63 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ o e. J /\ z e. X ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
64 63 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ o e. J ) /\ z e. X ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
65 64 an32s 
 |-  ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ o e. J ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
66 65 adantlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
67 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ o e. J /\ w e. X ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
68 67 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ o e. J ) /\ w e. X ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
69 68 an32s 
 |-  ( ( ( J e. ( TopOn ` X ) /\ w e. X ) /\ o e. J ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
70 69 adantllr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
71 66 70 imbi12d 
 |-  ( ( ( ( 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 ) ) ) )
72 62 71 sylibrd 
 |-  ( ( ( ( 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 ) ) )
73 72 ralrimdva 
 |-  ( ( ( 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 ) ) )
74 1 kqfval 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X ) -> ( F ` z ) = { y e. J | z e. y } )
75 74 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( F ` z ) = { y e. J | z e. y } )
76 1 kqfval 
 |-  ( ( J e. ( TopOn ` X ) /\ w e. X ) -> ( F ` w ) = { y e. J | w e. y } )
77 76 adantlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( F ` w ) = { y e. J | w e. y } )
78 75 77 eqeq12d 
 |-  ( ( ( 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 } ) )
79 rabbi 
 |-  ( A. y e. J ( z e. y <-> w e. y ) <-> { y e. J | z e. y } = { y e. J | w e. y } )
80 49 79 bitri 
 |-  ( A. o e. J ( z e. o <-> w e. o ) <-> { y e. J | z e. y } = { y e. J | w e. y } )
81 78 80 bitr4di 
 |-  ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. o e. J ( z e. o <-> w e. o ) ) )
82 81 biimprd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( A. o e. J ( z e. o <-> w e. o ) -> ( F ` z ) = ( F ` w ) ) )
83 73 82 imim12d 
 |-  ( ( ( 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 ) ) ) )
84 83 ralimdva 
 |-  ( ( 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 ) ) ) )
85 84 ralimdva 
 |-  ( 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 ) ) ) )
86 eleq1 
 |-  ( a = ( F ` z ) -> ( a e. v <-> ( F ` z ) e. v ) )
87 86 imbi1d 
 |-  ( a = ( F ` z ) -> ( ( a e. v -> b e. v ) <-> ( ( F ` z ) e. v -> b e. v ) ) )
88 87 ralbidv 
 |-  ( 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 ) ) )
89 eqeq1 
 |-  ( a = ( F ` z ) -> ( a = b <-> ( F ` z ) = b ) )
90 88 89 imbi12d 
 |-  ( 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 ) ) )
91 90 ralbidv 
 |-  ( 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 ) ) )
92 91 ralrn 
 |-  ( 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 ) ) )
93 eleq1 
 |-  ( b = ( F ` w ) -> ( b e. v <-> ( F ` w ) e. v ) )
94 93 imbi2d 
 |-  ( b = ( F ` w ) -> ( ( ( F ` z ) e. v -> b e. v ) <-> ( ( F ` z ) e. v -> ( F ` w ) e. v ) ) )
95 94 ralbidv 
 |-  ( 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 ) ) )
96 eqeq2 
 |-  ( b = ( F ` w ) -> ( ( F ` z ) = b <-> ( F ` z ) = ( F ` w ) ) )
97 95 96 imbi12d 
 |-  ( 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 ) ) ) )
98 97 ralrn 
 |-  ( 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 ) ) ) )
99 98 ralbidv 
 |-  ( 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 ) ) ) )
100 92 99 bitrd 
 |-  ( 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 ) ) ) )
101 11 100 syl 
 |-  ( 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 ) ) ) )
102 85 101 sylibrd 
 |-  ( 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 ) ) )
103 ist1-2 
 |-  ( ( 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 ) ) )
104 33 103 syl 
 |-  ( 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 ) ) )
105 102 104 sylibrd 
 |-  ( 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 ) )
106 55 105 impbid 
 |-  ( 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 ) ) ) )