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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion isr0 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( KQ ‘ 𝐽 ) ∈ Fre ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) ) )

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 1 kqid ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
3 2 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
4 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑣 ) ∈ 𝐽 )
5 3 4 sylan ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑣 ) ∈ 𝐽 )
6 eleq2 ⊢ ( 𝑜 = ( ◡ 𝐹 “ 𝑣 ) → ( 𝑧 ∈ 𝑜 ↔ 𝑧 ∈ ( ◡ 𝐹 “ 𝑣 ) ) )
7 eleq2 ⊢ ( 𝑜 = ( ◡ 𝐹 “ 𝑣 ) → ( 𝑤 ∈ 𝑜 ↔ 𝑤 ∈ ( ◡ 𝐹 “ 𝑣 ) ) )
8 6 7 imbi12d ⊢ ( 𝑜 = ( ◡ 𝐹 “ 𝑣 ) → ( ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) ↔ ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑣 ) → 𝑤 ∈ ( ◡ 𝐹 “ 𝑣 ) ) ) )
9 8 rspcv ⊢ ( ( ◡ 𝐹 “ 𝑣 ) ∈ 𝐽 → ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑣 ) → 𝑤 ∈ ( ◡ 𝐹 “ 𝑣 ) ) ) )
10 5 9 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑣 ) → 𝑤 ∈ ( ◡ 𝐹 “ 𝑣 ) ) ) )
11 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
12 11 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐹 Fn 𝑋 )
13 12 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → 𝐹 Fn 𝑋 )
14 fnfun ⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 )
15 13 14 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → Fun 𝐹 )
16 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
17 16 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → 𝑧 ∈ 𝑋 )
18 13 fndmd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → dom 𝐹 = 𝑋 )
19 17 18 eleqtrrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → 𝑧 ∈ dom 𝐹 )
20 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 ↔ 𝑧 ∈ ( ◡ 𝐹 “ 𝑣 ) ) )
21 15 19 20 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 ↔ 𝑧 ∈ ( ◡ 𝐹 “ 𝑣 ) ) )
22 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑤 ∈ 𝑋 )
23 22 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → 𝑤 ∈ 𝑋 )
24 23 18 eleqtrrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → 𝑤 ∈ dom 𝐹 )
25 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ↔ 𝑤 ∈ ( ◡ 𝐹 “ 𝑣 ) ) )
26 15 24 25 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ↔ 𝑤 ∈ ( ◡ 𝐹 “ 𝑣 ) ) )
27 21 26 imbi12d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) ↔ ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑣 ) → 𝑤 ∈ ( ◡ 𝐹 “ 𝑣 ) ) ) )
28 10 27 sylibrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑣 ∈ ( KQ ‘ 𝐽 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) ) )
29 28 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) ) )
30 simplr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( KQ ‘ 𝐽 ) ∈ Fre )
31 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
32 12 16 31 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
33 1 kqtopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
34 33 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
35 toponuni ⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ran 𝐹 = ∪ ( KQ ‘ 𝐽 ) )
36 34 35 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ran 𝐹 = ∪ ( KQ ‘ 𝐽 ) )
37 32 36 eleqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ∪ ( KQ ‘ 𝐽 ) )
38 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑤 ) ∈ ran 𝐹 )
39 12 22 38 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ran 𝐹 )
40 39 36 eleqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ∪ ( KQ ‘ 𝐽 ) )
41 eqid ⊢ ∪ ( KQ ‘ 𝐽 ) = ∪ ( KQ ‘ 𝐽 )
42 41 t1sep2 ⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Fre ∧ ( 𝐹 ‘ 𝑧 ) ∈ ∪ ( KQ ‘ 𝐽 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ ∪ ( KQ ‘ 𝐽 ) ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
43 30 37 40 42 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
44 29 43 syld ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
45 1 kqfeq ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ) )
46 eleq2 ⊢ ( 𝑜 = 𝑦 → ( 𝑧 ∈ 𝑜 ↔ 𝑧 ∈ 𝑦 ) )
47 eleq2 ⊢ ( 𝑜 = 𝑦 → ( 𝑤 ∈ 𝑜 ↔ 𝑤 ∈ 𝑦 ) )
48 46 47 bibi12d ⊢ ( 𝑜 = 𝑦 → ( ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ↔ ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ) )
49 48 cbvralvw ⊢ ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) )
50 45 49 bitr4di ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) )
51 50 3expb ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) )
52 51 adantlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) )
53 44 52 sylibd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) )
54 53 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) )
55 54 ex ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( KQ ‘ 𝐽 ) ∈ Fre → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) ) )
56 1 kqopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝐹 “ 𝑜 ) ∈ ( KQ ‘ 𝐽 ) )
57 56 ad4ant14 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝐹 “ 𝑜 ) ∈ ( KQ ‘ 𝐽 ) )
58 eleq2 ⊢ ( 𝑣 = ( 𝐹 “ 𝑜 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) ) )
59 eleq2 ⊢ ( 𝑣 = ( 𝐹 “ 𝑜 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) )
60 58 59 imbi12d ⊢ ( 𝑣 = ( 𝐹 “ 𝑜 ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) ) )
61 60 rspcv ⊢ ( ( 𝐹 “ 𝑜 ) ∈ ( KQ ‘ 𝐽 ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) ) )
62 57 61 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) ) )
63 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) ) )
64 63 3expa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) ) )
65 64 an32s ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑧 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) ) )
66 65 adantlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑧 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) ) )
67 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) )
68 67 3expa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) )
69 68 an32s ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑤 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) )
70 69 adantllr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑤 ∈ 𝑜 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) )
71 66 70 imbi12d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑜 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑜 ) ) ) )
72 62 71 sylibrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) ) )
73 72 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) ) )
74 1 kqfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) = { 𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦 } )
75 74 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) = { 𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦 } )
76 1 kqfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑤 ) = { 𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦 } )
77 76 adantlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑤 ) = { 𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦 } )
78 75 77 eqeq12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ { 𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦 } ) )
79 rabbi ⊢ ( ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ↔ { 𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦 } )
80 49 79 bitri ⊢ ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ↔ { 𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦 } )
81 78 80 bitr4di ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) )
82 81 biimprd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
83 73 82 imim12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
84 83 ralimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) → ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
85 84 ralimdva ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
86 eleq1 ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( 𝑎 ∈ 𝑣 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 ) )
87 86 imbi1d ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) ) )
88 87 ralbidv ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) ↔ ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) ) )
89 eqeq1 ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( 𝑎 = 𝑏 ↔ ( 𝐹 ‘ 𝑧 ) = 𝑏 ) )
90 88 89 imbi12d ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ↔ ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = 𝑏 ) ) )
91 90 ralbidv ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ↔ ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = 𝑏 ) ) )
92 91 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = 𝑏 ) ) )
93 eleq1 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( 𝑏 ∈ 𝑣 ↔ ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) )
94 93 imbi2d ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) ) )
95 94 ralbidv ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) ↔ ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) ) )
96 eqeq2 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑏 ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
97 95 96 imbi12d ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = 𝑏 ) ↔ ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
98 97 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = 𝑏 ) ↔ ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
99 98 ralbidv ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = 𝑏 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
100 92 99 bitrd ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
101 11 100 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑣 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
102 85 101 sylibrd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) → ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ) )
103 ist1-2 ⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ( ( KQ ‘ 𝐽 ) ∈ Fre ↔ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ) )
104 33 103 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( KQ ‘ 𝐽 ) ∈ Fre ↔ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ∀ 𝑣 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣 ) → 𝑎 = 𝑏 ) ) )
105 102 104 sylibrd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) → ( KQ ‘ 𝐽 ) ∈ Fre ) )
106 55 105 impbid ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( KQ ‘ 𝐽 ) ∈ Fre ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜 ) ) ) )