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

Theorem isr0 22888
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 22879 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
32ad2antrr 723 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
4 cnima 22416 . . . . . . . . . 10 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (𝐹𝑣) ∈ 𝐽)
53, 4sylan 580 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (𝐹𝑣) ∈ 𝐽)
6 eleq2 2827 . . . . . . . . . . 11 (𝑜 = (𝐹𝑣) → (𝑧𝑜𝑧 ∈ (𝐹𝑣)))
7 eleq2 2827 . . . . . . . . . . 11 (𝑜 = (𝐹𝑣) → (𝑤𝑜𝑤 ∈ (𝐹𝑣)))
86, 7imbi12d 345 . . . . . . . . . 10 (𝑜 = (𝐹𝑣) → ((𝑧𝑜𝑤𝑜) ↔ (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
98rspcv 3557 . . . . . . . . 9 ((𝐹𝑣) ∈ 𝐽 → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
105, 9syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
111kqffn 22876 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
1211ad2antrr 723 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝐹 Fn 𝑋)
1312adantr 481 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
14 fnfun 6533 . . . . . . . . . . 11 (𝐹 Fn 𝑋 → Fun 𝐹)
1513, 14syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → Fun 𝐹)
16 simprl 768 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝑧𝑋)
1716adantr 481 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧𝑋)
1813fndmd 6538 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → dom 𝐹 = 𝑋)
1917, 18eleqtrrd 2842 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧 ∈ dom 𝐹)
20 fvimacnv 6930 . . . . . . . . . 10 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑣𝑧 ∈ (𝐹𝑣)))
2115, 19, 20syl2anc 584 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹𝑧) ∈ 𝑣𝑧 ∈ (𝐹𝑣)))
22 simprr 770 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → 𝑤𝑋)
2322adantr 481 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤𝑋)
2423, 18eleqtrrd 2842 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤 ∈ dom 𝐹)
25 fvimacnv 6930 . . . . . . . . . 10 ((Fun 𝐹𝑤 ∈ dom 𝐹) → ((𝐹𝑤) ∈ 𝑣𝑤 ∈ (𝐹𝑣)))
2615, 24, 25syl2anc 584 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹𝑤) ∈ 𝑣𝑤 ∈ (𝐹𝑣)))
2721, 26imbi12d 345 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) ↔ (𝑧 ∈ (𝐹𝑣) → 𝑤 ∈ (𝐹𝑣))))
2810, 27sylibrd 258 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
2928ralrimdva 3106 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
30 simplr 766 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (KQ‘𝐽) ∈ Fre)
31 fnfvelrn 6958 . . . . . . . . 9 ((𝐹 Fn 𝑋𝑧𝑋) → (𝐹𝑧) ∈ ran 𝐹)
3212, 16, 31syl2anc 584 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑧) ∈ ran 𝐹)
331kqtopon 22878 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3433ad2antrr 723 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
35 toponuni 22063 . . . . . . . . 9 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = (KQ‘𝐽))
3634, 35syl 17 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → ran 𝐹 = (KQ‘𝐽))
3732, 36eleqtrd 2841 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑧) ∈ (KQ‘𝐽))
38 fnfvelrn 6958 . . . . . . . . 9 ((𝐹 Fn 𝑋𝑤𝑋) → (𝐹𝑤) ∈ ran 𝐹)
3912, 22, 38syl2anc 584 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑤) ∈ ran 𝐹)
4039, 36eleqtrd 2841 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (𝐹𝑤) ∈ (KQ‘𝐽))
41 eqid 2738 . . . . . . . 8 (KQ‘𝐽) = (KQ‘𝐽)
4241t1sep2 22520 . . . . . . 7 (((KQ‘𝐽) ∈ Fre ∧ (𝐹𝑧) ∈ (KQ‘𝐽) ∧ (𝐹𝑤) ∈ (KQ‘𝐽)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤)))
4330, 37, 40, 42syl3anc 1370 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤)))
4429, 43syld 47 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝐹𝑧) = (𝐹𝑤)))
451kqfeq 22875 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑦𝐽 (𝑧𝑦𝑤𝑦)))
46 eleq2 2827 . . . . . . . . . 10 (𝑜 = 𝑦 → (𝑧𝑜𝑧𝑦))
47 eleq2 2827 . . . . . . . . . 10 (𝑜 = 𝑦 → (𝑤𝑜𝑤𝑦))
4846, 47bibi12d 346 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝑧𝑜𝑤𝑜) ↔ (𝑧𝑦𝑤𝑦)))
4948cbvralvw 3383 . . . . . . . 8 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) ↔ ∀𝑦𝐽 (𝑧𝑦𝑤𝑦))
5045, 49bitr4di 289 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
51503expb 1119 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑧𝑋𝑤𝑋)) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5251adantlr 712 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5344, 52sylibd 238 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧𝑋𝑤𝑋)) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5453ralrimivva 3123 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) → ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
5554ex 413 . 2 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre → ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜))))
561kqopn 22885 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) → (𝐹𝑜) ∈ (KQ‘𝐽))
5756ad4ant14 749 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝐹𝑜) ∈ (KQ‘𝐽))
58 eleq2 2827 . . . . . . . . . . . 12 (𝑣 = (𝐹𝑜) → ((𝐹𝑧) ∈ 𝑣 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
59 eleq2 2827 . . . . . . . . . . . 12 (𝑣 = (𝐹𝑜) → ((𝐹𝑤) ∈ 𝑣 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
6058, 59imbi12d 345 . . . . . . . . . . 11 (𝑣 = (𝐹𝑜) → (((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) ↔ ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
6160rspcv 3557 . . . . . . . . . 10 ((𝐹𝑜) ∈ (KQ‘𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
6257, 61syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
631kqfvima 22881 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽𝑧𝑋) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
64633expa 1117 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) ∧ 𝑧𝑋) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
6564an32s 649 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑜𝐽) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
6665adantlr 712 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑧𝑜 ↔ (𝐹𝑧) ∈ (𝐹𝑜)))
671kqfvima 22881 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽𝑤𝑋) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
68673expa 1117 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜𝐽) ∧ 𝑤𝑋) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
6968an32s 649 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7069adantllr 716 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (𝑤𝑜 ↔ (𝐹𝑤) ∈ (𝐹𝑜)))
7166, 70imbi12d 345 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → ((𝑧𝑜𝑤𝑜) ↔ ((𝐹𝑧) ∈ (𝐹𝑜) → (𝐹𝑤) ∈ (𝐹𝑜))))
7262, 71sylibrd 258 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) ∧ 𝑜𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝑧𝑜𝑤𝑜)))
7372ralrimdva 3106 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
741kqfval 22874 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) → (𝐹𝑧) = {𝑦𝐽𝑧𝑦})
7574adantr 481 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (𝐹𝑧) = {𝑦𝐽𝑧𝑦})
761kqfval 22874 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝑋) → (𝐹𝑤) = {𝑦𝐽𝑤𝑦})
7776adantlr 712 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (𝐹𝑤) = {𝑦𝐽𝑤𝑦})
7875, 77eqeq12d 2754 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦}))
79 rabbi 3316 . . . . . . . . . 10 (∀𝑦𝐽 (𝑧𝑦𝑤𝑦) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦})
8049, 79bitri 274 . . . . . . . . 9 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) ↔ {𝑦𝐽𝑧𝑦} = {𝑦𝐽𝑤𝑦})
8178, 80bitr4di 289 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((𝐹𝑧) = (𝐹𝑤) ↔ ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)))
8281biimprd 247 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → (𝐹𝑧) = (𝐹𝑤)))
8373, 82imim12d 81 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) ∧ 𝑤𝑋) → ((∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
8483ralimdva 3108 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋) → (∀𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
8584ralimdva 3108 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
86 eleq1 2826 . . . . . . . . . . 11 (𝑎 = (𝐹𝑧) → (𝑎𝑣 ↔ (𝐹𝑧) ∈ 𝑣))
8786imbi1d 342 . . . . . . . . . 10 (𝑎 = (𝐹𝑧) → ((𝑎𝑣𝑏𝑣) ↔ ((𝐹𝑧) ∈ 𝑣𝑏𝑣)))
8887ralbidv 3112 . . . . . . . . 9 (𝑎 = (𝐹𝑧) → (∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣)))
89 eqeq1 2742 . . . . . . . . 9 (𝑎 = (𝐹𝑧) → (𝑎 = 𝑏 ↔ (𝐹𝑧) = 𝑏))
9088, 89imbi12d 345 . . . . . . . 8 (𝑎 = (𝐹𝑧) → ((∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
9190ralbidv 3112 . . . . . . 7 (𝑎 = (𝐹𝑧) → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
9291ralrn 6964 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏)))
93 eleq1 2826 . . . . . . . . . . 11 (𝑏 = (𝐹𝑤) → (𝑏𝑣 ↔ (𝐹𝑤) ∈ 𝑣))
9493imbi2d 341 . . . . . . . . . 10 (𝑏 = (𝐹𝑤) → (((𝐹𝑧) ∈ 𝑣𝑏𝑣) ↔ ((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
9594ralbidv 3112 . . . . . . . . 9 (𝑏 = (𝐹𝑤) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣)))
96 eqeq2 2750 . . . . . . . . 9 (𝑏 = (𝐹𝑤) → ((𝐹𝑧) = 𝑏 ↔ (𝐹𝑧) = (𝐹𝑤)))
9795, 96imbi12d 345 . . . . . . . 8 (𝑏 = (𝐹𝑤) → ((∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
9897ralrn 6964 . . . . . . 7 (𝐹 Fn 𝑋 → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ ∀𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
9998ralbidv 3112 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑧𝑋𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣𝑏𝑣) → (𝐹𝑧) = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10092, 99bitrd 278 . . . . 5 (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10111, 100syl 17 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑣 → (𝐹𝑤) ∈ 𝑣) → (𝐹𝑧) = (𝐹𝑤))))
10285, 101sylibrd 258 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
103 ist1-2 22498 . . . 4 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
10433, 103syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎𝑣𝑏𝑣) → 𝑎 = 𝑏)))
105102, 104sylibrd 258 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜)) → (KQ‘𝐽) ∈ Fre))
10655, 105impbid 211 1 (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑧𝑋𝑤𝑋 (∀𝑜𝐽 (𝑧𝑜𝑤𝑜) → ∀𝑜𝐽 (𝑧𝑜𝑤𝑜))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  wral 3064  {crab 3068   cuni 4839  cmpt 5157  ccnv 5588  dom cdm 5589  ran crn 5590  cima 5592  Fun wfun 6427   Fn wfn 6428  cfv 6433  (class class class)co 7275  TopOnctopon 22059   Cn ccn 22375  Frect1 22458  KQckq 22844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-map 8617  df-topgen 17154  df-qtop 17218  df-top 22043  df-topon 22060  df-cld 22170  df-cn 22378  df-t1 22465  df-kq 22845
This theorem is referenced by:  r0sep  22899
  Copyright terms: Public domain W3C validator