Metamath Proof Explorer


Theorem r0cld

Description: The analogue of the T_1 axiom (singletons are closed) for an R_0 space. In an R_0 space the set of all points topologically indistinguishable from A is closed. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 𝐹 = ( 𝑥𝑋 ↦ { 𝑦𝐽𝑥𝑦 } )
Assertion r0cld ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → { 𝑧𝑋 ∣ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) } ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 kqval.2 𝐹 = ( 𝑥𝑋 ↦ { 𝑦𝐽𝑥𝑦 } )
2 1 kqffn ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
3 2 3ad2ant1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → 𝐹 Fn 𝑋 )
4 fncnvima2 ( 𝐹 Fn 𝑋 → ( 𝐹 “ { ( 𝐹𝐴 ) } ) = { 𝑧𝑋 ∣ ( 𝐹𝑧 ) ∈ { ( 𝐹𝐴 ) } } )
5 3 4 syl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ( 𝐹 “ { ( 𝐹𝐴 ) } ) = { 𝑧𝑋 ∣ ( 𝐹𝑧 ) ∈ { ( 𝐹𝐴 ) } } )
6 fvex ( 𝐹𝑧 ) ∈ V
7 6 elsn ( ( 𝐹𝑧 ) ∈ { ( 𝐹𝐴 ) } ↔ ( 𝐹𝑧 ) = ( 𝐹𝐴 ) )
8 simpl1 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) ∧ 𝑧𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9 simpr ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) ∧ 𝑧𝑋 ) → 𝑧𝑋 )
10 simpl3 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) ∧ 𝑧𝑋 ) → 𝐴𝑋 )
11 1 kqfeq ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧𝑋𝐴𝑋 ) → ( ( 𝐹𝑧 ) = ( 𝐹𝐴 ) ↔ ∀ 𝑦𝐽 ( 𝑧𝑦𝐴𝑦 ) ) )
12 eleq2w ( 𝑦 = 𝑜 → ( 𝑧𝑦𝑧𝑜 ) )
13 eleq2w ( 𝑦 = 𝑜 → ( 𝐴𝑦𝐴𝑜 ) )
14 12 13 bibi12d ( 𝑦 = 𝑜 → ( ( 𝑧𝑦𝐴𝑦 ) ↔ ( 𝑧𝑜𝐴𝑜 ) ) )
15 14 cbvralvw ( ∀ 𝑦𝐽 ( 𝑧𝑦𝐴𝑦 ) ↔ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) )
16 11 15 bitrdi ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧𝑋𝐴𝑋 ) → ( ( 𝐹𝑧 ) = ( 𝐹𝐴 ) ↔ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) ) )
17 8 9 10 16 syl3anc ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) ∧ 𝑧𝑋 ) → ( ( 𝐹𝑧 ) = ( 𝐹𝐴 ) ↔ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) ) )
18 7 17 syl5bb ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) ∧ 𝑧𝑋 ) → ( ( 𝐹𝑧 ) ∈ { ( 𝐹𝐴 ) } ↔ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) ) )
19 18 rabbidva ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → { 𝑧𝑋 ∣ ( 𝐹𝑧 ) ∈ { ( 𝐹𝐴 ) } } = { 𝑧𝑋 ∣ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) } )
20 5 19 eqtrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ( 𝐹 “ { ( 𝐹𝐴 ) } ) = { 𝑧𝑋 ∣ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) } )
21 1 kqid ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
22 21 3ad2ant1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
23 simp2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ( KQ ‘ 𝐽 ) ∈ Fre )
24 simp3 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → 𝐴𝑋 )
25 fnfvelrn ( ( 𝐹 Fn 𝑋𝐴𝑋 ) → ( 𝐹𝐴 ) ∈ ran 𝐹 )
26 3 24 25 syl2anc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ( 𝐹𝐴 ) ∈ ran 𝐹 )
27 1 kqtopon ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
28 27 3ad2ant1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
29 toponuni ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ran 𝐹 = ( KQ ‘ 𝐽 ) )
30 28 29 syl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ran 𝐹 = ( KQ ‘ 𝐽 ) )
31 26 30 eleqtrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ( 𝐹𝐴 ) ∈ ( KQ ‘ 𝐽 ) )
32 eqid ( KQ ‘ 𝐽 ) = ( KQ ‘ 𝐽 )
33 32 t1sncld ( ( ( KQ ‘ 𝐽 ) ∈ Fre ∧ ( 𝐹𝐴 ) ∈ ( KQ ‘ 𝐽 ) ) → { ( 𝐹𝐴 ) } ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
34 23 31 33 syl2anc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → { ( 𝐹𝐴 ) } ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
35 cnclima ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ { ( 𝐹𝐴 ) } ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) → ( 𝐹 “ { ( 𝐹𝐴 ) } ) ∈ ( Clsd ‘ 𝐽 ) )
36 22 34 35 syl2anc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → ( 𝐹 “ { ( 𝐹𝐴 ) } ) ∈ ( Clsd ‘ 𝐽 ) )
37 20 36 eqeltrrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴𝑋 ) → { 𝑧𝑋 ∣ ∀ 𝑜𝐽 ( 𝑧𝑜𝐴𝑜 ) } ∈ ( Clsd ‘ 𝐽 ) )