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 bitrid ⊢ ( ( ( 𝐽 ∈ ( 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 ‘ 𝐽 ) )