isr0 - Metamath Proof Explorer

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

Theorem isr0 21953

Description: The property "𝐽 is an R₀ space". A space is R₀ 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 R₀ if and only if its Kolmogorov quotient is T₁, 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.

Step	Hyp	Ref	Expression
1		kqval.2	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
2	1	kqid 21944	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
3	2	ad2antrr 716	. . . . . . . . . 10 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
4		cnima 21481	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑣) ∈ 𝐽)
5	3, 4	sylan 575	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑣) ∈ 𝐽)
6		eleq2 2848	. . . . . . . . . . 11 ⊢ (𝑜 = (^◡𝐹 “ 𝑣) → (𝑧 ∈ 𝑜 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑣)))
7		eleq2 2848	. . . . . . . . . . 11 ⊢ (𝑜 = (^◡𝐹 “ 𝑣) → (𝑤 ∈ 𝑜 ↔ 𝑤 ∈ (^◡𝐹 “ 𝑣)))
8	6, 7	imbi12d 336	. . . . . . . . . 10 ⊢ (𝑜 = (^◡𝐹 “ 𝑣) → ((𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) ↔ (𝑧 ∈ (^◡𝐹 “ 𝑣) → 𝑤 ∈ (^◡𝐹 “ 𝑣))))
9	8	rspcv 3507	. . . . . . . . 9 ⊢ ((^◡𝐹 “ 𝑣) ∈ 𝐽 → (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → (𝑧 ∈ (^◡𝐹 “ 𝑣) → 𝑤 ∈ (^◡𝐹 “ 𝑣))))
10	5, 9	syl 17	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → (𝑧 ∈ (^◡𝐹 “ 𝑣) → 𝑤 ∈ (^◡𝐹 “ 𝑣))))
11	1	kqffn 21941	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
12	11	ad2antrr 716	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝐹 Fn 𝑋)
13	12	adantr 474	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
14		fnfun 6235	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
15	13, 14	syl 17	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → Fun 𝐹)
16		simprl 761	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝑧 ∈ 𝑋)
17	16	adantr 474	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧 ∈ 𝑋)
18		fndm 6237	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
19	13, 18	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → dom 𝐹 = 𝑋)
20	17, 19	eleqtrrd 2862	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑧 ∈ dom 𝐹)
21		fvimacnv 6597	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑣 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑣)))
22	15, 20, 21	syl2anc 579	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹‘𝑧) ∈ 𝑣 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑣)))
23		simprr 763	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝑤 ∈ 𝑋)
24	23	adantr 474	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤 ∈ 𝑋)
25	24, 19	eleqtrrd 2862	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → 𝑤 ∈ dom 𝐹)
26		fvimacnv 6597	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹) → ((𝐹‘𝑤) ∈ 𝑣 ↔ 𝑤 ∈ (^◡𝐹 “ 𝑣)))
27	15, 25, 26	syl2anc 579	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → ((𝐹‘𝑤) ∈ 𝑣 ↔ 𝑤 ∈ (^◡𝐹 “ 𝑣)))
28	22, 27	imbi12d 336	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) ↔ (𝑧 ∈ (^◡𝐹 “ 𝑣) → 𝑤 ∈ (^◡𝐹 “ 𝑣))))
29	10, 28	sylibrd 251	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑣 ∈ (KQ‘𝐽)) → (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣)))
30	29	ralrimdva 3151	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣)))
31		simplr 759	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (KQ‘𝐽) ∈ Fre)
32		fnfvelrn 6622	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ran 𝐹)
33	12, 16, 32	syl2anc 579	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑧) ∈ ran 𝐹)
34	1	kqtopon 21943	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
35	34	ad2antrr 716	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
36		toponuni 21130	. . . . . . . . 9 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = ∪ (KQ‘𝐽))
37	35, 36	syl 17	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ran 𝐹 = ∪ (KQ‘𝐽))
38	33, 37	eleqtrd 2861	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑧) ∈ ∪ (KQ‘𝐽))
39		fnfvelrn 6622	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝐹‘𝑤) ∈ ran 𝐹)
40	12, 23, 39	syl2anc 579	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ∈ ran 𝐹)
41	40, 37	eleqtrd 2861	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ∈ ∪ (KQ‘𝐽))
42		eqid 2778	. . . . . . . 8 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
43	42	t1sep2 21585	. . . . . . 7 ⊢ (((KQ‘𝐽) ∈ Fre ∧ (𝐹‘𝑧) ∈ ∪ (KQ‘𝐽) ∧ (𝐹‘𝑤) ∈ ∪ (KQ‘𝐽)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤)))
44	31, 38, 41, 43	syl3anc 1439	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤)))
45	30, 44	syld 47	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → (𝐹‘𝑧) = (𝐹‘𝑤)))
46	1	kqfeq 21940	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ∀𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦)))
47		eleq2 2848	. . . . . . . . . 10 ⊢ (𝑜 = 𝑦 → (𝑧 ∈ 𝑜 ↔ 𝑧 ∈ 𝑦))
48		eleq2 2848	. . . . . . . . . 10 ⊢ (𝑜 = 𝑦 → (𝑤 ∈ 𝑜 ↔ 𝑤 ∈ 𝑦))
49	47, 48	bibi12d 337	. . . . . . . . 9 ⊢ (𝑜 = 𝑦 → ((𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜) ↔ (𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦)))
50	49	cbvralv 3367	. . . . . . . 8 ⊢ (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜) ↔ ∀𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦))
51	46, 50	syl6bbr 281	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))
52	51	3expb 1110	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))
53	52	adantlr 705	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))
54	45, 53	sylibd 231	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))
55	54	ralrimivva 3153	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) → ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))
56	55	ex 403	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre → ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜))))
57		simpll 757	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
58	1	kqopn 21950	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜 ∈ 𝐽) → (𝐹 “ 𝑜) ∈ (KQ‘𝐽))
59	57, 58	sylan 575	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → (𝐹 “ 𝑜) ∈ (KQ‘𝐽))
60		eleq2 2848	. . . . . . . . . . . 12 ⊢ (𝑣 = (𝐹 “ 𝑜) → ((𝐹‘𝑧) ∈ 𝑣 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑜)))
61		eleq2 2848	. . . . . . . . . . . 12 ⊢ (𝑣 = (𝐹 “ 𝑜) → ((𝐹‘𝑤) ∈ 𝑣 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑜)))
62	60, 61	imbi12d 336	. . . . . . . . . . 11 ⊢ (𝑣 = (𝐹 “ 𝑜) → (((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑜) → (𝐹‘𝑤) ∈ (𝐹 “ 𝑜))))
63	62	rspcv 3507	. . . . . . . . . 10 ⊢ ((𝐹 “ 𝑜) ∈ (KQ‘𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑜) → (𝐹‘𝑤) ∈ (𝐹 “ 𝑜))))
64	59, 63	syl 17	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑜) → (𝐹‘𝑤) ∈ (𝐹 “ 𝑜))))
65	1	kqfvima 21946	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ 𝑜 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑜)))
66	65	3expa 1108	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜 ∈ 𝐽) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ 𝑜 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑜)))
67	66	an32s 642	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → (𝑧 ∈ 𝑜 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑜)))
68	67	adantlr 705	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → (𝑧 ∈ 𝑜 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑜)))
69	1	kqfvima 21946	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜 ∈ 𝐽 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝑜 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑜)))
70	69	3expa 1108	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑜 ∈ 𝐽) ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝑜 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑜)))
71	70	an32s 642	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → (𝑤 ∈ 𝑜 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑜)))
72	71	adantllr 709	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → (𝑤 ∈ 𝑜 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑜)))
73	68, 72	imbi12d 336	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → ((𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑜) → (𝐹‘𝑤) ∈ (𝐹 “ 𝑜))))
74	64, 73	sylibrd 251	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜)))
75	74	ralrimdva 3151	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜)))
76	1	kqfval 21939	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = {𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦})
77	76	adantr 474	. . . . . . . . . 10 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐹‘𝑧) = {𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦})
78	1	kqfval 21939	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐹‘𝑤) = {𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦})
79	78	adantlr 705	. . . . . . . . . 10 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐹‘𝑤) = {𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦})
80	77, 79	eqeq12d 2793	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ {𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦} = {𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦}))
81		rabbi 3307	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦) ↔ {𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦} = {𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦})
82	50, 81	bitri 267	. . . . . . . . 9 ⊢ (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜) ↔ {𝑦 ∈ 𝐽 ∣ 𝑧 ∈ 𝑦} = {𝑦 ∈ 𝐽 ∣ 𝑤 ∈ 𝑦})
83	80, 82	syl6bbr 281	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))
84	83	biimprd 240	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜) → (𝐹‘𝑧) = (𝐹‘𝑤)))
85	75, 84	imim12d 81	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → ((∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
86	85	ralimdva 3144	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋) → (∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)) → ∀𝑤 ∈ 𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
87	86	ralimdva 3144	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)) → ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
88		eleq1 2847	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐹‘𝑧) → (𝑎 ∈ 𝑣 ↔ (𝐹‘𝑧) ∈ 𝑣))
89	88	imbi1d 333	. . . . . . . . . 10 ⊢ (𝑎 = (𝐹‘𝑧) → ((𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) ↔ ((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣)))
90	89	ralbidv 3168	. . . . . . . . 9 ⊢ (𝑎 = (𝐹‘𝑧) → (∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣)))
91		eqeq1 2782	. . . . . . . . 9 ⊢ (𝑎 = (𝐹‘𝑧) → (𝑎 = 𝑏 ↔ (𝐹‘𝑧) = 𝑏))
92	90, 91	imbi12d 336	. . . . . . . 8 ⊢ (𝑎 = (𝐹‘𝑧) → ((∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) → (𝐹‘𝑧) = 𝑏)))
93	92	ralbidv 3168	. . . . . . 7 ⊢ (𝑎 = (𝐹‘𝑧) → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏) ↔ ∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) → (𝐹‘𝑧) = 𝑏)))
94	93	ralrn 6628	. . . . . 6 ⊢ (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧 ∈ 𝑋 ∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) → (𝐹‘𝑧) = 𝑏)))
95		eleq1 2847	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐹‘𝑤) → (𝑏 ∈ 𝑣 ↔ (𝐹‘𝑤) ∈ 𝑣))
96	95	imbi2d 332	. . . . . . . . . 10 ⊢ (𝑏 = (𝐹‘𝑤) → (((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) ↔ ((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣)))
97	96	ralbidv 3168	. . . . . . . . 9 ⊢ (𝑏 = (𝐹‘𝑤) → (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) ↔ ∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣)))
98		eqeq2 2789	. . . . . . . . 9 ⊢ (𝑏 = (𝐹‘𝑤) → ((𝐹‘𝑧) = 𝑏 ↔ (𝐹‘𝑧) = (𝐹‘𝑤)))
99	97, 98	imbi12d 336	. . . . . . . 8 ⊢ (𝑏 = (𝐹‘𝑤) → ((∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) → (𝐹‘𝑧) = 𝑏) ↔ (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
100	99	ralrn 6628	. . . . . . 7 ⊢ (𝐹 Fn 𝑋 → (∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) → (𝐹‘𝑧) = 𝑏) ↔ ∀𝑤 ∈ 𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
101	100	ralbidv 3168	. . . . . 6 ⊢ (𝐹 Fn 𝑋 → (∀𝑧 ∈ 𝑋 ∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → 𝑏 ∈ 𝑣) → (𝐹‘𝑧) = 𝑏) ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
102	94, 101	bitrd 271	. . . . 5 ⊢ (𝐹 Fn 𝑋 → (∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
103	11, 102	syl 17	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏) ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑣 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑣 → (𝐹‘𝑤) ∈ 𝑣) → (𝐹‘𝑧) = (𝐹‘𝑤))))
104	87, 103	sylibrd 251	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)) → ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏)))
105		ist1-2 21563	. . . 4 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏)))
106	34, 105	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(∀𝑣 ∈ (KQ‘𝐽)(𝑎 ∈ 𝑣 → 𝑏 ∈ 𝑣) → 𝑎 = 𝑏)))
107	104, 106	sylibrd 251	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)) → (KQ‘𝐽) ∈ Fre))
108	56, 107	impbid 204	1 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∧ w3a 1071 = wceq 1601 ∈ wcel 2107 ∀wral 3090 {crab 3094 ∪ cuni 4673 ↦ cmpt 4967 ^◡ccnv 5356 dom cdm 5357 ran crn 5358 “ cima 5360 Fun wfun 6131 Fn wfn 6132 ‘cfv 6137 (class class class)co 6924 TopOnctopon 21126 Cn ccn 21440 Frect1 21523 KQckq 21909

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5008 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-iun 4757 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 df-ov 6927 df-oprab 6928 df-mpt2 6929 df-map 8144 df-topgen 16494 df-qtop 16557 df-top 21110 df-topon 21127 df-cld 21235 df-cn 21443 df-t1 21530 df-kq 21910

This theorem is referenced by: r0sep 21964

W3C validator