Metamath Proof Explorer

Theorem istopclsd

Description: A closure function which satisfies sscls , clsidm , cls0 , and clsun defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses istopclsd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
istopclsd.f ⊢ ( 𝜑 → 𝐹 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
istopclsd.e ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
istopclsd.i ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
istopclsd.z ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
istopclsd.u ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐹 ‘ 𝑦 ) ) )
istopclsd.j ⊢ 𝐽 = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐹 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝐵 ∖ 𝑧 ) }
Assertion istopclsd ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ ( cls ‘ 𝐽 ) = 𝐹 ) )

Proof

Step Hyp Ref Expression
1 istopclsd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2 istopclsd.f ⊢ ( 𝜑 → 𝐹 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
3 istopclsd.e ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
4 istopclsd.i ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
5 istopclsd.z ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
6 istopclsd.u ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐹 ‘ 𝑦 ) ) )
7 istopclsd.j ⊢ 𝐽 = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐹 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝐵 ∖ 𝑧 ) }
8 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝒫 𝐵 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → 𝐹 Fn 𝒫 𝐵 )
10 difss ⊢ ( 𝐵 ∖ 𝑧 ) ⊆ 𝐵
11 elpw2g ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝒫 𝐵 ↔ ( 𝐵 ∖ 𝑧 ) ⊆ 𝐵 ) )
12 1 11 syl ⊢ ( 𝜑 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝒫 𝐵 ↔ ( 𝐵 ∖ 𝑧 ) ⊆ 𝐵 ) )
13 10 12 mpbiri ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑧 ) ∈ 𝒫 𝐵 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑧 ) ∈ 𝒫 𝐵 )
15 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ ( 𝐵 ∖ 𝑧 ) ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝐵 ∖ 𝑧 ) ) )
16 9 14 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝐵 ∖ 𝑧 ) ) )
17 16 bicomd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( 𝐹 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝐵 ∖ 𝑧 ) ↔ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ) )
18 17 rabbidva ⊢ ( 𝜑 → { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐹 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝐵 ∖ 𝑧 ) } = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } )
19 7 18 eqtrid ⊢ ( 𝜑 → 𝐽 = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } )
20 simp1 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → 𝜑 )
21 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → 𝑥 ⊆ 𝐵 )
22 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ⊆ 𝑥 )
23 22 21 sstrd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ⊆ 𝐵 )
24 20 21 23 6 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐹 ‘ 𝑦 ) ) )
25 ssequn2 ⊢ ( 𝑦 ⊆ 𝑥 ↔ ( 𝑥 ∪ 𝑦 ) = 𝑥 )
26 25 biimpi ⊢ ( 𝑦 ⊆ 𝑥 → ( 𝑥 ∪ 𝑦 ) = 𝑥 )
27 26 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑥 ∪ 𝑦 ) = 𝑥 )
28 27 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( 𝐹 ‘ 𝑥 ) )
29 24 28 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ 𝑥 ) )
30 ssequn2 ⊢ ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ 𝑥 ) )
31 29 30 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
32 1 2 3 31 4 ismrcd1 ⊢ ( 𝜑 → dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) )
33 0elpw ⊢ ∅ ∈ 𝒫 𝐵
34 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ ∅ ∈ 𝒫 𝐵 ) → ( ∅ ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ∅ ) = ∅ ) )
35 8 33 34 sylancl ⊢ ( 𝜑 → ( ∅ ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ∅ ) = ∅ ) )
36 5 35 mpbird ⊢ ( 𝜑 → ∅ ∈ dom ( 𝐹 ∩ I ) )
37 simp1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝜑 )
38 inss1 ⊢ ( 𝐹 ∩ I ) ⊆ 𝐹
39 dmss ⊢ ( ( 𝐹 ∩ I ) ⊆ 𝐹 → dom ( 𝐹 ∩ I ) ⊆ dom 𝐹 )
40 38 39 ax-mp ⊢ dom ( 𝐹 ∩ I ) ⊆ dom 𝐹
41 40 2 fssdm ⊢ ( 𝜑 → dom ( 𝐹 ∩ I ) ⊆ 𝒫 𝐵 )
42 41 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → dom ( 𝐹 ∩ I ) ⊆ 𝒫 𝐵 )
43 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝑥 ∈ dom ( 𝐹 ∩ I ) )
44 42 43 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝑥 ∈ 𝒫 𝐵 )
45 44 elpwid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝑥 ⊆ 𝐵 )
46 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝑦 ∈ dom ( 𝐹 ∩ I ) )
47 42 46 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝑦 ∈ 𝒫 𝐵 )
48 47 elpwid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝑦 ⊆ 𝐵 )
49 37 45 48 6 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐹 ‘ 𝑦 ) ) )
50 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → 𝐹 Fn 𝒫 𝐵 )
51 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
52 50 44 51 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝑥 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
53 43 52 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
54 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ 𝑦 ∈ 𝒫 𝐵 ) → ( 𝑦 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) )
55 50 47 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝑦 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) )
56 46 55 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝐹 ‘ 𝑦 ) = 𝑦 )
57 53 56 uneq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∪ 𝑦 ) )
58 49 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑥 ∪ 𝑦 ) )
59 45 48 unssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝑥 ∪ 𝑦 ) ⊆ 𝐵 )
60 vex ⊢ 𝑥 ∈ V
61 vex ⊢ 𝑦 ∈ V
62 60 61 unex ⊢ ( 𝑥 ∪ 𝑦 ) ∈ V
63 62 elpw ⊢ ( ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐵 ↔ ( 𝑥 ∪ 𝑦 ) ⊆ 𝐵 )
64 59 63 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐵 )
65 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐵 ) → ( ( 𝑥 ∪ 𝑦 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑥 ∪ 𝑦 ) ) )
66 50 64 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( ( 𝑥 ∪ 𝑦 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑥 ∪ 𝑦 ) ) )
67 58 66 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ∧ 𝑦 ∈ dom ( 𝐹 ∩ I ) ) → ( 𝑥 ∪ 𝑦 ) ∈ dom ( 𝐹 ∩ I ) )
68 eqid ⊢ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) }
69 32 36 67 68 mretopd ⊢ ( 𝜑 → ( { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } ∈ ( TopOn ‘ 𝐵 ) ∧ dom ( 𝐹 ∩ I ) = ( Clsd ‘ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } ) ) )
70 69 simpld ⊢ ( 𝜑 → { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } ∈ ( TopOn ‘ 𝐵 ) )
71 19 70 eqeltrd ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
72 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐽 ∈ Top )
73 71 72 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
74 eqid ⊢ ( mrCls ‘ ( Clsd ‘ 𝐽 ) ) = ( mrCls ‘ ( Clsd ‘ 𝐽 ) )
75 74 mrccls ⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = ( mrCls ‘ ( Clsd ‘ 𝐽 ) ) )
76 73 75 syl ⊢ ( 𝜑 → ( cls ‘ 𝐽 ) = ( mrCls ‘ ( Clsd ‘ 𝐽 ) ) )
77 69 simprd ⊢ ( 𝜑 → dom ( 𝐹 ∩ I ) = ( Clsd ‘ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } ) )
78 19 fveq2d ⊢ ( 𝜑 → ( Clsd ‘ 𝐽 ) = ( Clsd ‘ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) } ) )
79 77 78 eqtr4d ⊢ ( 𝜑 → dom ( 𝐹 ∩ I ) = ( Clsd ‘ 𝐽 ) )
80 79 fveq2d ⊢ ( 𝜑 → ( mrCls ‘ dom ( 𝐹 ∩ I ) ) = ( mrCls ‘ ( Clsd ‘ 𝐽 ) ) )
81 76 80 eqtr4d ⊢ ( 𝜑 → ( cls ‘ 𝐽 ) = ( mrCls ‘ dom ( 𝐹 ∩ I ) ) )
82 1 2 3 31 4 ismrcd2 ⊢ ( 𝜑 → 𝐹 = ( mrCls ‘ dom ( 𝐹 ∩ I ) ) )
83 81 82 eqtr4d ⊢ ( 𝜑 → ( cls ‘ 𝐽 ) = 𝐹 )
84 71 83 jca ⊢ ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ ( cls ‘ 𝐽 ) = 𝐹 ) )