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

Theorem isr0 22337
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 22328 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
32ad2antrr 724 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
4 cnima 21865 . . . . . . . . . 10 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (𝐹𝑣) ∈ 𝐽)
53, 4sylan 582 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (𝐹𝑣) ∈ 𝐽)
6 eleq2 2899 . . . . . . . . . . 11 (𝑜 = (𝐹𝑣) → (𝑧𝑜𝑧 ∈ (𝐹𝑣)))
7 eleq2 2899 . . . . . . . . . . 11 (𝑜 = (𝐹𝑣) → (𝑤𝑜𝑤 ∈ (𝐹𝑣)))
86, 7imbi12d 347 . . . . . . . . . 10 (𝑜 = (𝐹𝑣) → ((𝑧𝑜𝑤𝑜) ↔ (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
98rspcv 3616 . . . . . . . . 9 ((𝐹𝑣) ∈ 𝐽 → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
105, 9syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
111kqffn 22325 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
1211ad2antrr 724 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝐹 Fn 𝑋)
1312adantr 483 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
14 fnfun 6446 . . . . . . . . . . 11 (𝐹 Fn 𝑋 → Fun 𝐹)
1513, 14syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → Fun 𝐹)
16 simprl 769 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝑧𝑋)
1716adantr 483 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧𝑋)
18 fndm 6448 . . . . . . . . . . . 12 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
1913, 18syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → dom 𝐹 = 𝑋)
2017, 19eleqtrrd 2914 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧 ∈ dom 𝐹)
21 fvimacnv 6816 . . . . . . . . . 10 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑣𝑧 ∈ (𝐹𝑣)))
2215, 20, 21syl2anc 586 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹𝑧) ∈ 𝑣𝑧 ∈ (𝐹𝑣)))
23 simprr 771 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝑤𝑋)
2423adantr 483 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤𝑋)
2524, 19eleqtrrd 2914 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤 ∈ dom 𝐹)
26 fvimacnv 6816 . . . . . . . . . 10 ((Fun 𝐹𝑤 ∈ dom 𝐹) → ((𝐹𝑤) ∈ 𝑣𝑤 ∈ (𝐹𝑣)))
2715, 25, 26syl2anc 586 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹𝑤) ∈ 𝑣𝑤 ∈ (𝐹𝑣)))
2822, 27imbi12d 347 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) ↔ (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
2910, 28sylibrd 261 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
3029ralrimdva 3187 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
31 simplr 767 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (KQ‘𝐽) ∈ Fre)
32 fnfvelrn 6841 . . . . . . . . 9 ((𝐹 Fn 𝑋𝑧𝑋) → (𝐹𝑧) ∈ ran 𝐹)
3312, 16, 32syl2anc 586 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑧) ∈ ran 𝐹)
341kqtopon 22327 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3534ad2antrr 724 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
36 toponuni 21514 . . . . . . . . 9 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = (KQ‘𝐽))
3735, 36syl 17 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → ran 𝐹 = (KQ‘𝐽))
3833, 37eleqtrd 2913 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑧) ∈ (KQ‘𝐽))
39 fnfvelrn 6841 . . . . . . . . 9 ((𝐹 Fn 𝑋𝑤𝑋) → (𝐹𝑤) ∈ ran 𝐹)
4012, 23, 39syl2anc 586 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑤) ∈ ran 𝐹)
4140, 37eleqtrd 2913 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑤) ∈ (KQ‘𝐽))
42 eqid 2819 . . . . . . . 8 (KQ‘𝐽) = (KQ‘𝐽)
4342t1sep2 21969 . . . . . . 7 (((KQ‘𝐽) ∈ Fre ∧ (𝐹𝑧) ∈ (KQ‘𝐽) ∧ (𝐹𝑤) ∈ (KQ‘𝐽)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤)))
4431, 38, 41, 43syl3anc 1365 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤)))
4530, 44syld 47 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝐹𝑧) = (𝐹𝑤)))
461kqfeq 22324 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑦𝐽 (𝑧𝑦𝑤𝑦)))
47 eleq2 2899 . . . . . . . . . 10 (𝑜 = 𝑦 → (𝑧𝑜𝑧𝑦))
48 eleq2 2899 . . . . . . . . . 10 (𝑜 = 𝑦 → (𝑤𝑜𝑤𝑦))
4947, 48bibi12d 348 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝑧𝑜𝑤𝑜) ↔ (𝑧𝑦𝑤𝑦)))
5049cbvralvw 3448 . . . . . . . 8 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) ↔ ∀𝑦𝐽 (𝑧𝑦𝑤𝑦))
5146, 50syl6bbr 291 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
52513expb 1114 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑧𝑋𝑤𝑋)) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5352adantlr 713 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5445, 53sylibd 241 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5554ralrimivva 3189 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) → ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5655ex 415 . 2 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre → ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜))))
571kqopn 22334 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) → (𝐹𝑜) ∈ (KQ‘𝐽))
5857ad4ant14 750 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝐹𝑜) ∈ (KQ‘𝐽))
59 eleq2 2899 . . . . . . . . . . . 12 (𝑣 = (𝐹𝑜) → ((𝐹𝑧) ∈ 𝑣 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
60 eleq2 2899 . . . . . . . . . . . 12 (𝑣 = (𝐹𝑜) → ((𝐹𝑤) ∈ 𝑣 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
6159, 60imbi12d 347 . . . . . . . . . . 11 (𝑣 = (𝐹𝑜) → (((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) ↔ ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
6261rspcv 3616 . . . . . . . . . 10 ((𝐹𝑜) ∈ (KQ‘𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
6358, 62syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
641kqfvima 22330 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽𝑧𝑋) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
65643expa 1112 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) ∧ 𝑧𝑋) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
6665an32s 650 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑜𝐽) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
6766adantlr 713 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
681kqfvima 22330 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽𝑤𝑋) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
69683expa 1112 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) ∧ 𝑤𝑋) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7069an32s 650 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7170adantllr 717 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7267, 71imbi12d 347 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → ((𝑧𝑜𝑤𝑜) ↔ ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
7363, 72sylibrd 261 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝑧𝑜𝑤𝑜)))
7473ralrimdva 3187 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
751kqfval 22323 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) → (𝐹𝑧) = {𝑦𝐽𝑧𝑦})
7675adantr 483 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (𝐹𝑧) = {𝑦𝐽𝑧𝑦})
771kqfval 22323 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝑋) → (𝐹𝑤) = {𝑦𝐽𝑤𝑦})
7877adantlr 713 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (𝐹𝑤) = {𝑦𝐽𝑤𝑦})
7976, 78eqeq12d 2835 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦}))
80 rabbi 3382 . . . . . . . . . 10 (∀𝑦𝐽 (𝑧𝑦𝑤𝑦) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦})
8150, 80bitri 277 . . . . . . . . 9 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦})
8279, 81syl6bbr 291 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
8382biimprd 250 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝐹𝑧) = (𝐹𝑤)))
8474, 83imim12d 81 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
8584ralimdva 3175 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) → (∀𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
8685ralimdva 3175 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
87 eleq1 2898 . . . . . . . . . . 11 (𝑎 = (𝐹𝑧) → (𝑎𝑣 ↔ (𝐹𝑧) ∈ 𝑣))
8887imbi1d 344 . . . . . . . . . 10 (𝑎 = (𝐹𝑧) → ((𝑎𝑣𝑏𝑣) ↔ ((𝐹𝑧) ∈ 𝑣𝑏𝑣)))
8988ralbidv 3195 . . . . . . . . 9 (𝑎 = (𝐹𝑧) → (∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣)))
90 eqeq1 2823 . . . . . . . . 9 (𝑎 = (𝐹𝑧) → (𝑎 = 𝑏 ↔ (𝐹𝑧) = 𝑏))
9189, 90imbi12d 347 . . . . . . . 8 (𝑎 = (𝐹𝑧) → ((∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
9291ralbidv 3195 . . . . . . 7 (𝑎 = (𝐹𝑧) → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
9392ralrn 6847 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
94 eleq1 2898 . . . . . . . . . . 11 (𝑏 = (𝐹𝑤) → (𝑏𝑣 ↔ (𝐹𝑤) ∈ 𝑣))
9594imbi2d 343 . . . . . . . . . 10 (𝑏 = (𝐹𝑤) → (((𝐹𝑧) ∈ 𝑣𝑏𝑣) ↔ ((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
9695ralbidv 3195 . . . . . . . . 9 (𝑏 = (𝐹𝑤) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
97 eqeq2 2831 . . . . . . . . 9 (𝑏 = (𝐹𝑤) → ((𝐹𝑧) = 𝑏 ↔ (𝐹𝑧) = (𝐹𝑤)))
9896, 97imbi12d 347 . . . . . . . 8 (𝑏 = (𝐹𝑤) → ((∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
9998ralrn 6847 . . . . . . 7 (𝐹 Fn 𝑋 → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ ∀𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10099ralbidv 3195 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑧𝑋𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10193, 100bitrd 281 . . . . 5 (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10211, 101syl 17 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10386, 102sylibrd 261 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
104 ist1-2 21947 . . . 4 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
10534, 104syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
106103, 105sylibrd 261 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → (KQ‘𝐽) ∈ Fre))
10756, 106impbid 214 1 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1081   = wceq 1530  wcel 2107  wral 3136  {crab 3140   cuni 4830  cmpt 5137  ccnv 5547  dom cdm 5548  ran crn 5549  cima 5551  Fun wfun 6342   Fn wfn 6343  cfv 6348  (class class class)co 7148  TopOnctopon 21510   Cn ccn 21824  Frect1 21907  KQckq 22293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-map 8400  df-topgen 16709  df-qtop 16772  df-top 21494  df-topon 21511  df-cld 21619  df-cn 21827  df-t1 21914  df-kq 22294
This theorem is referenced by:  r0sep  22348
  Copyright terms: Public domain W3C validator