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 
|- ( ph -> B e. V )
istopclsd.f 
|- ( ph -> F : ~P B --> ~P B )
istopclsd.e 
|- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
istopclsd.i 
|- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )
istopclsd.z 
|- ( ph -> ( F ` (/) ) = (/) )
istopclsd.u 
|- ( ( ph /\ x C_ B /\ y C_ B ) -> ( F ` ( x u. y ) ) = ( ( F ` x ) u. ( F ` y ) ) )
istopclsd.j 
|- J = { z e. ~P B | ( F ` ( B \ z ) ) = ( B \ z ) }
Assertion istopclsd 
|- ( ph -> ( J e. ( TopOn ` B ) /\ ( cls ` J ) = F ) )

Proof

Step Hyp Ref Expression
1 istopclsd.b 
 |-  ( ph -> B e. V )
2 istopclsd.f 
 |-  ( ph -> F : ~P B --> ~P B )
3 istopclsd.e 
 |-  ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
4 istopclsd.i 
 |-  ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )
5 istopclsd.z 
 |-  ( ph -> ( F ` (/) ) = (/) )
6 istopclsd.u 
 |-  ( ( ph /\ x C_ B /\ y C_ B ) -> ( F ` ( x u. y ) ) = ( ( F ` x ) u. ( F ` y ) ) )
7 istopclsd.j 
 |-  J = { z e. ~P B | ( F ` ( B \ z ) ) = ( B \ z ) }
8 2 ffnd 
 |-  ( ph -> F Fn ~P B )
9 8 adantr 
 |-  ( ( ph /\ z e. ~P B ) -> F Fn ~P B )
10 difss 
 |-  ( B \ z ) C_ B
11 elpw2g 
 |-  ( B e. V -> ( ( B \ z ) e. ~P B <-> ( B \ z ) C_ B ) )
12 1 11 syl 
 |-  ( ph -> ( ( B \ z ) e. ~P B <-> ( B \ z ) C_ B ) )
13 10 12 mpbiri 
 |-  ( ph -> ( B \ z ) e. ~P B )
14 13 adantr 
 |-  ( ( ph /\ z e. ~P B ) -> ( B \ z ) e. ~P B )
15 fnelfp 
 |-  ( ( F Fn ~P B /\ ( B \ z ) e. ~P B ) -> ( ( B \ z ) e. dom ( F i^i _I ) <-> ( F ` ( B \ z ) ) = ( B \ z ) ) )
16 9 14 15 syl2anc 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( B \ z ) e. dom ( F i^i _I ) <-> ( F ` ( B \ z ) ) = ( B \ z ) ) )
17 16 bicomd 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( F ` ( B \ z ) ) = ( B \ z ) <-> ( B \ z ) e. dom ( F i^i _I ) ) )
18 17 rabbidva 
 |-  ( ph -> { z e. ~P B | ( F ` ( B \ z ) ) = ( B \ z ) } = { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } )
19 7 18 syl5eq 
 |-  ( ph -> J = { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } )
20 simp1 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ph )
21 simp2 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> x C_ B )
22 simp3 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> y C_ x )
23 22 21 sstrd 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> y C_ B )
24 20 21 23 6 syl3anc 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` ( x u. y ) ) = ( ( F ` x ) u. ( F ` y ) ) )
25 ssequn2 
 |-  ( y C_ x <-> ( x u. y ) = x )
26 25 biimpi 
 |-  ( y C_ x -> ( x u. y ) = x )
27 26 3ad2ant3 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ( x u. y ) = x )
28 27 fveq2d 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` ( x u. y ) ) = ( F ` x ) )
29 24 28 eqtr3d 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ( ( F ` x ) u. ( F ` y ) ) = ( F ` x ) )
30 ssequn2 
 |-  ( ( F ` y ) C_ ( F ` x ) <-> ( ( F ` x ) u. ( F ` y ) ) = ( F ` x ) )
31 29 30 sylibr 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )
32 1 2 3 31 4 ismrcd1 
 |-  ( ph -> dom ( F i^i _I ) e. ( Moore ` B ) )
33 0elpw 
 |-  (/) e. ~P B
34 fnelfp 
 |-  ( ( F Fn ~P B /\ (/) e. ~P B ) -> ( (/) e. dom ( F i^i _I ) <-> ( F ` (/) ) = (/) ) )
35 8 33 34 sylancl 
 |-  ( ph -> ( (/) e. dom ( F i^i _I ) <-> ( F ` (/) ) = (/) ) )
36 5 35 mpbird 
 |-  ( ph -> (/) e. dom ( F i^i _I ) )
37 simp1 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ph )
38 inss1 
 |-  ( F i^i _I ) C_ F
39 dmss 
 |-  ( ( F i^i _I ) C_ F -> dom ( F i^i _I ) C_ dom F )
40 38 39 ax-mp 
 |-  dom ( F i^i _I ) C_ dom F
41 40 2 fssdm 
 |-  ( ph -> dom ( F i^i _I ) C_ ~P B )
42 41 3ad2ant1 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> dom ( F i^i _I ) C_ ~P B )
43 simp2 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> x e. dom ( F i^i _I ) )
44 42 43 sseldd 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> x e. ~P B )
45 44 elpwid 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> x C_ B )
46 simp3 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> y e. dom ( F i^i _I ) )
47 42 46 sseldd 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> y e. ~P B )
48 47 elpwid 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> y C_ B )
49 37 45 48 6 syl3anc 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( F ` ( x u. y ) ) = ( ( F ` x ) u. ( F ` y ) ) )
50 8 3ad2ant1 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> F Fn ~P B )
51 fnelfp 
 |-  ( ( F Fn ~P B /\ x e. ~P B ) -> ( x e. dom ( F i^i _I ) <-> ( F ` x ) = x ) )
52 50 44 51 syl2anc 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( x e. dom ( F i^i _I ) <-> ( F ` x ) = x ) )
53 43 52 mpbid 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( F ` x ) = x )
54 fnelfp 
 |-  ( ( F Fn ~P B /\ y e. ~P B ) -> ( y e. dom ( F i^i _I ) <-> ( F ` y ) = y ) )
55 50 47 54 syl2anc 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( y e. dom ( F i^i _I ) <-> ( F ` y ) = y ) )
56 46 55 mpbid 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( F ` y ) = y )
57 53 56 uneq12d 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( ( F ` x ) u. ( F ` y ) ) = ( x u. y ) )
58 49 57 eqtrd 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( F ` ( x u. y ) ) = ( x u. y ) )
59 45 48 unssd 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( x u. y ) C_ B )
60 vex 
 |-  x e. _V
61 vex 
 |-  y e. _V
62 60 61 unex 
 |-  ( x u. y ) e. _V
63 62 elpw 
 |-  ( ( x u. y ) e. ~P B <-> ( x u. y ) C_ B )
64 59 63 sylibr 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( x u. y ) e. ~P B )
65 fnelfp 
 |-  ( ( F Fn ~P B /\ ( x u. y ) e. ~P B ) -> ( ( x u. y ) e. dom ( F i^i _I ) <-> ( F ` ( x u. y ) ) = ( x u. y ) ) )
66 50 64 65 syl2anc 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( ( x u. y ) e. dom ( F i^i _I ) <-> ( F ` ( x u. y ) ) = ( x u. y ) ) )
67 58 66 mpbird 
 |-  ( ( ph /\ x e. dom ( F i^i _I ) /\ y e. dom ( F i^i _I ) ) -> ( x u. y ) e. dom ( F i^i _I ) )
68 eqid 
 |-  { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } = { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) }
69 32 36 67 68 mretopd 
 |-  ( ph -> ( { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } e. ( TopOn ` B ) /\ dom ( F i^i _I ) = ( Clsd ` { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } ) ) )
70 69 simpld 
 |-  ( ph -> { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } e. ( TopOn ` B ) )
71 19 70 eqeltrd 
 |-  ( ph -> J e. ( TopOn ` B ) )
72 topontop 
 |-  ( J e. ( TopOn ` B ) -> J e. Top )
73 71 72 syl 
 |-  ( ph -> J e. Top )
74 eqid 
 |-  ( mrCls ` ( Clsd ` J ) ) = ( mrCls ` ( Clsd ` J ) )
75 74 mrccls 
 |-  ( J e. Top -> ( cls ` J ) = ( mrCls ` ( Clsd ` J ) ) )
76 73 75 syl 
 |-  ( ph -> ( cls ` J ) = ( mrCls ` ( Clsd ` J ) ) )
77 69 simprd 
 |-  ( ph -> dom ( F i^i _I ) = ( Clsd ` { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } ) )
78 19 fveq2d 
 |-  ( ph -> ( Clsd ` J ) = ( Clsd ` { z e. ~P B | ( B \ z ) e. dom ( F i^i _I ) } ) )
79 77 78 eqtr4d 
 |-  ( ph -> dom ( F i^i _I ) = ( Clsd ` J ) )
80 79 fveq2d 
 |-  ( ph -> ( mrCls ` dom ( F i^i _I ) ) = ( mrCls ` ( Clsd ` J ) ) )
81 76 80 eqtr4d 
 |-  ( ph -> ( cls ` J ) = ( mrCls ` dom ( F i^i _I ) ) )
82 1 2 3 31 4 ismrcd2 
 |-  ( ph -> F = ( mrCls ` dom ( F i^i _I ) ) )
83 81 82 eqtr4d 
 |-  ( ph -> ( cls ` J ) = F )
84 71 83 jca 
 |-  ( ph -> ( J e. ( TopOn ` B ) /\ ( cls ` J ) = F ) )