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

Theorem isr0 21738
 Description: The property "𝐽 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 𝑥 also contains 𝑦, so there is no separation, then 𝑥 and 𝑦 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 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
Assertion
Ref Expression
isr0 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜))))
Distinct variable groups:   𝑤,𝑜,𝑥,𝑦,𝑧,𝐽   𝑜,𝐹,𝑤,𝑧   𝑜,𝑋,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem isr0
Dummy variables 𝑎 𝑏 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kqval.2 . . . . . . . . . . . 12 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
21kqid 21729 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
32ad2antrr 764 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
4 cnima 21267 . . . . . . . . . 10 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (𝐹𝑣) ∈ 𝐽)
53, 4sylan 489 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (𝐹𝑣) ∈ 𝐽)
6 eleq2 2824 . . . . . . . . . . 11 (𝑜 = (𝐹𝑣) → (𝑧𝑜𝑧 ∈ (𝐹𝑣)))
7 eleq2 2824 . . . . . . . . . . 11 (𝑜 = (𝐹𝑣) → (𝑤𝑜𝑤 ∈ (𝐹𝑣)))
86, 7imbi12d 333 . . . . . . . . . 10 (𝑜 = (𝐹𝑣) → ((𝑧𝑜𝑤𝑜) ↔ (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
98rspcv 3441 . . . . . . . . 9 ((𝐹𝑣) ∈ 𝐽 → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
105, 9syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
111kqffn 21726 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
1211ad2antrr 764 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝐹 Fn 𝑋)
1312adantr 472 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
14 fnfun 6145 . . . . . . . . . . 11 (𝐹 Fn 𝑋 → Fun 𝐹)
1513, 14syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → Fun 𝐹)
16 simprl 811 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝑧𝑋)
1716adantr 472 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧𝑋)
18 fndm 6147 . . . . . . . . . . . 12 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
1913, 18syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → dom 𝐹 = 𝑋)
2017, 19eleqtrrd 2838 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧 ∈ dom 𝐹)
21 fvimacnv 6491 . . . . . . . . . 10 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑣𝑧 ∈ (𝐹𝑣)))
2215, 20, 21syl2anc 696 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹𝑧) ∈ 𝑣𝑧 ∈ (𝐹𝑣)))
23 simprr 813 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝑤𝑋)
2423adantr 472 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤𝑋)
2524, 19eleqtrrd 2838 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤 ∈ dom 𝐹)
26 fvimacnv 6491 . . . . . . . . . 10 ((Fun 𝐹𝑤 ∈ dom 𝐹) → ((𝐹𝑤) ∈ 𝑣𝑤 ∈ (𝐹𝑣)))
2715, 25, 26syl2anc 696 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹𝑤) ∈ 𝑣𝑤 ∈ (𝐹𝑣)))
2822, 27imbi12d 333 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) ↔ (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
2910, 28sylibrd 249 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
3029ralrimdva 3103 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
31 simplr 809 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (KQ‘𝐽) ∈ Fre)
32 fnfvelrn 6515 . . . . . . . . 9 ((𝐹 Fn 𝑋𝑧𝑋) → (𝐹𝑧) ∈ ran 𝐹)
3312, 16, 32syl2anc 696 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑧) ∈ ran 𝐹)
341kqtopon 21728 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3534ad2antrr 764 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
36 toponuni 20917 . . . . . . . . 9 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = (KQ‘𝐽))
3735, 36syl 17 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → ran 𝐹 = (KQ‘𝐽))
3833, 37eleqtrd 2837 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑧) ∈ (KQ‘𝐽))
39 fnfvelrn 6515 . . . . . . . . 9 ((𝐹 Fn 𝑋𝑤𝑋) → (𝐹𝑤) ∈ ran 𝐹)
4012, 23, 39syl2anc 696 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑤) ∈ ran 𝐹)
4140, 37eleqtrd 2837 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑤) ∈ (KQ‘𝐽))
42 eqid 2756 . . . . . . . 8 (KQ‘𝐽) = (KQ‘𝐽)
4342t1sep2 21371 . . . . . . 7 (((KQ‘𝐽) ∈ Fre ∧ (𝐹𝑧) ∈ (KQ‘𝐽) ∧ (𝐹𝑤) ∈ (KQ‘𝐽)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤)))
4431, 38, 41, 43syl3anc 1477 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤)))
4530, 44syld 47 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝐹𝑧) = (𝐹𝑤)))
461kqfeq 21725 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑦𝐽 (𝑧𝑦𝑤𝑦)))
47 eleq2 2824 . . . . . . . . . 10 (𝑜 = 𝑦 → (𝑧𝑜𝑧𝑦))
48 eleq2 2824 . . . . . . . . . 10 (𝑜 = 𝑦 → (𝑤𝑜𝑤𝑦))
4947, 48bibi12d 334 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝑧𝑜𝑤𝑜) ↔ (𝑧𝑦𝑤𝑦)))
5049cbvralv 3306 . . . . . . . 8 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) ↔ ∀𝑦𝐽 (𝑧𝑦𝑤𝑦))
5146, 50syl6bbr 278 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
52513expb 1114 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑧𝑋𝑤𝑋)) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5352adantlr 753 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5445, 53sylibd 229 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5554ralrimivva 3105 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) → ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5655ex 449 . 2 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre → ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜))))
57 simpll 807 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → 𝐽 ∈ (TopOn‘𝑋))
581kqopn 21735 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) → (𝐹𝑜) ∈ (KQ‘𝐽))
5957, 58sylan 489 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝐹𝑜) ∈ (KQ‘𝐽))
60 eleq2 2824 . . . . . . . . . . . 12 (𝑣 = (𝐹𝑜) → ((𝐹𝑧) ∈ 𝑣 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
61 eleq2 2824 . . . . . . . . . . . 12 (𝑣 = (𝐹𝑜) → ((𝐹𝑤) ∈ 𝑣 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
6260, 61imbi12d 333 . . . . . . . . . . 11 (𝑣 = (𝐹𝑜) → (((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) ↔ ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
6362rspcv 3441 . . . . . . . . . 10 ((𝐹𝑜) ∈ (KQ‘𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
6459, 63syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
651kqfvima 21731 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽𝑧𝑋) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
66653expa 1112 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) ∧ 𝑧𝑋) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
6766an32s 881 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑜𝐽) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
6867adantlr 753 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
691kqfvima 21731 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽𝑤𝑋) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
70693expa 1112 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) ∧ 𝑤𝑋) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7170an32s 881 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7271adantllr 757 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7368, 72imbi12d 333 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → ((𝑧𝑜𝑤𝑜) ↔ ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
7464, 73sylibrd 249 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝑧𝑜𝑤𝑜)))
7574ralrimdva 3103 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
761kqfval 21724 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) → (𝐹𝑧) = {𝑦𝐽𝑧𝑦})
7776adantr 472 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (𝐹𝑧) = {𝑦𝐽𝑧𝑦})
781kqfval 21724 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝑋) → (𝐹𝑤) = {𝑦𝐽𝑤𝑦})
7978adantlr 753 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (𝐹𝑤) = {𝑦𝐽𝑤𝑦})
8077, 79eqeq12d 2771 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦}))
81 rabbi 3255 . . . . . . . . . 10 (∀𝑦𝐽 (𝑧𝑦𝑤𝑦) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦})
8250, 81bitri 264 . . . . . . . . 9 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦})
8380, 82syl6bbr 278 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
8483biimprd 238 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝐹𝑧) = (𝐹𝑤)))
8575, 84imim12d 81 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
8685ralimdva 3096 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) → (∀𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
8786ralimdva 3096 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
88 eleq1 2823 . . . . . . . . . . 11 (𝑎 = (𝐹𝑧) → (𝑎𝑣 ↔ (𝐹𝑧) ∈ 𝑣))
8988imbi1d 330 . . . . . . . . . 10 (𝑎 = (𝐹𝑧) → ((𝑎𝑣𝑏𝑣) ↔ ((𝐹𝑧) ∈ 𝑣𝑏𝑣)))
9089ralbidv 3120 . . . . . . . . 9 (𝑎 = (𝐹𝑧) → (∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣)))
91 eqeq1 2760 . . . . . . . . 9 (𝑎 = (𝐹𝑧) → (𝑎 = 𝑏 ↔ (𝐹𝑧) = 𝑏))
9290, 91imbi12d 333 . . . . . . . 8 (𝑎 = (𝐹𝑧) → ((∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
9392ralbidv 3120 . . . . . . 7 (𝑎 = (𝐹𝑧) → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
9493ralrn 6521 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
95 eleq1 2823 . . . . . . . . . . 11 (𝑏 = (𝐹𝑤) → (𝑏𝑣 ↔ (𝐹𝑤) ∈ 𝑣))
9695imbi2d 329 . . . . . . . . . 10 (𝑏 = (𝐹𝑤) → (((𝐹𝑧) ∈ 𝑣𝑏𝑣) ↔ ((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
9796ralbidv 3120 . . . . . . . . 9 (𝑏 = (𝐹𝑤) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
98 eqeq2 2767 . . . . . . . . 9 (𝑏 = (𝐹𝑤) → ((𝐹𝑧) = 𝑏 ↔ (𝐹𝑧) = (𝐹𝑤)))
9997, 98imbi12d 333 . . . . . . . 8 (𝑏 = (𝐹𝑤) → ((∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10099ralrn 6521 . . . . . . 7 (𝐹 Fn 𝑋 → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ ∀𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
101100ralbidv 3120 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑧𝑋𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10294, 101bitrd 268 . . . . 5 (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10311, 102syl 17 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10487, 103sylibrd 249 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
105 ist1-2 21349 . . . 4 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
10634, 105syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
107104, 106sylibrd 249 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → (KQ‘𝐽) ∈ Fre))
10856, 107impbid 202 1 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1628   ∈ wcel 2135  ∀wral 3046  {crab 3050  ∪ cuni 4584   ↦ cmpt 4877  ◡ccnv 5261  dom cdm 5262  ran crn 5263   “ cima 5265  Fun wfun 6039   Fn wfn 6040  ‘cfv 6045  (class class class)co 6809  TopOnctopon 20913   Cn ccn 21226  Frect1 21309  KQckq 21694 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-map 8021  df-topgen 16302  df-qtop 16365  df-top 20897  df-topon 20914  df-cld 21021  df-cn 21229  df-t1 21316  df-kq 21695 This theorem is referenced by:  r0sep  21749
 Copyright terms: Public domain W3C validator