Metamath Proof Explorer


Theorem indistopon

Description: The indiscrete topology on a set A . Part of Example 2 in Munkres p. 77. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion indistopon
|- ( A e. V -> { (/) , A } e. ( TopOn ` A ) )

Proof

Step Hyp Ref Expression
1 sspr
 |-  ( x C_ { (/) , A } <-> ( ( x = (/) \/ x = { (/) } ) \/ ( x = { A } \/ x = { (/) , A } ) ) )
2 unieq
 |-  ( x = (/) -> U. x = U. (/) )
3 uni0
 |-  U. (/) = (/)
4 0ex
 |-  (/) e. _V
5 4 prid1
 |-  (/) e. { (/) , A }
6 3 5 eqeltri
 |-  U. (/) e. { (/) , A }
7 2 6 eqeltrdi
 |-  ( x = (/) -> U. x e. { (/) , A } )
8 7 a1i
 |-  ( A e. V -> ( x = (/) -> U. x e. { (/) , A } ) )
9 unieq
 |-  ( x = { (/) } -> U. x = U. { (/) } )
10 4 unisn
 |-  U. { (/) } = (/)
11 10 5 eqeltri
 |-  U. { (/) } e. { (/) , A }
12 9 11 eqeltrdi
 |-  ( x = { (/) } -> U. x e. { (/) , A } )
13 12 a1i
 |-  ( A e. V -> ( x = { (/) } -> U. x e. { (/) , A } ) )
14 8 13 jaod
 |-  ( A e. V -> ( ( x = (/) \/ x = { (/) } ) -> U. x e. { (/) , A } ) )
15 unieq
 |-  ( x = { A } -> U. x = U. { A } )
16 unisng
 |-  ( A e. V -> U. { A } = A )
17 15 16 sylan9eqr
 |-  ( ( A e. V /\ x = { A } ) -> U. x = A )
18 prid2g
 |-  ( A e. V -> A e. { (/) , A } )
19 18 adantr
 |-  ( ( A e. V /\ x = { A } ) -> A e. { (/) , A } )
20 17 19 eqeltrd
 |-  ( ( A e. V /\ x = { A } ) -> U. x e. { (/) , A } )
21 20 ex
 |-  ( A e. V -> ( x = { A } -> U. x e. { (/) , A } ) )
22 unieq
 |-  ( x = { (/) , A } -> U. x = U. { (/) , A } )
23 uniprg
 |-  ( ( (/) e. _V /\ A e. V ) -> U. { (/) , A } = ( (/) u. A ) )
24 4 23 mpan
 |-  ( A e. V -> U. { (/) , A } = ( (/) u. A ) )
25 uncom
 |-  ( (/) u. A ) = ( A u. (/) )
26 un0
 |-  ( A u. (/) ) = A
27 25 26 eqtri
 |-  ( (/) u. A ) = A
28 24 27 eqtrdi
 |-  ( A e. V -> U. { (/) , A } = A )
29 22 28 sylan9eqr
 |-  ( ( A e. V /\ x = { (/) , A } ) -> U. x = A )
30 18 adantr
 |-  ( ( A e. V /\ x = { (/) , A } ) -> A e. { (/) , A } )
31 29 30 eqeltrd
 |-  ( ( A e. V /\ x = { (/) , A } ) -> U. x e. { (/) , A } )
32 31 ex
 |-  ( A e. V -> ( x = { (/) , A } -> U. x e. { (/) , A } ) )
33 21 32 jaod
 |-  ( A e. V -> ( ( x = { A } \/ x = { (/) , A } ) -> U. x e. { (/) , A } ) )
34 14 33 jaod
 |-  ( A e. V -> ( ( ( x = (/) \/ x = { (/) } ) \/ ( x = { A } \/ x = { (/) , A } ) ) -> U. x e. { (/) , A } ) )
35 1 34 syl5bi
 |-  ( A e. V -> ( x C_ { (/) , A } -> U. x e. { (/) , A } ) )
36 35 alrimiv
 |-  ( A e. V -> A. x ( x C_ { (/) , A } -> U. x e. { (/) , A } ) )
37 vex
 |-  x e. _V
38 37 elpr
 |-  ( x e. { (/) , A } <-> ( x = (/) \/ x = A ) )
39 vex
 |-  y e. _V
40 39 elpr
 |-  ( y e. { (/) , A } <-> ( y = (/) \/ y = A ) )
41 simpr
 |-  ( ( x = (/) /\ y = (/) ) -> y = (/) )
42 41 ineq2d
 |-  ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) = ( x i^i (/) ) )
43 in0
 |-  ( x i^i (/) ) = (/)
44 42 43 eqtrdi
 |-  ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) = (/) )
45 44 5 eqeltrdi
 |-  ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } )
46 45 a1i
 |-  ( A e. V -> ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } ) )
47 simpr
 |-  ( ( x = A /\ y = (/) ) -> y = (/) )
48 47 ineq2d
 |-  ( ( x = A /\ y = (/) ) -> ( x i^i y ) = ( x i^i (/) ) )
49 48 43 eqtrdi
 |-  ( ( x = A /\ y = (/) ) -> ( x i^i y ) = (/) )
50 49 5 eqeltrdi
 |-  ( ( x = A /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } )
51 50 a1i
 |-  ( A e. V -> ( ( x = A /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } ) )
52 simpl
 |-  ( ( x = (/) /\ y = A ) -> x = (/) )
53 52 ineq1d
 |-  ( ( x = (/) /\ y = A ) -> ( x i^i y ) = ( (/) i^i y ) )
54 0in
 |-  ( (/) i^i y ) = (/)
55 53 54 eqtrdi
 |-  ( ( x = (/) /\ y = A ) -> ( x i^i y ) = (/) )
56 55 5 eqeltrdi
 |-  ( ( x = (/) /\ y = A ) -> ( x i^i y ) e. { (/) , A } )
57 56 a1i
 |-  ( A e. V -> ( ( x = (/) /\ y = A ) -> ( x i^i y ) e. { (/) , A } ) )
58 ineq12
 |-  ( ( x = A /\ y = A ) -> ( x i^i y ) = ( A i^i A ) )
59 58 adantl
 |-  ( ( A e. V /\ ( x = A /\ y = A ) ) -> ( x i^i y ) = ( A i^i A ) )
60 inidm
 |-  ( A i^i A ) = A
61 59 60 eqtrdi
 |-  ( ( A e. V /\ ( x = A /\ y = A ) ) -> ( x i^i y ) = A )
62 18 adantr
 |-  ( ( A e. V /\ ( x = A /\ y = A ) ) -> A e. { (/) , A } )
63 61 62 eqeltrd
 |-  ( ( A e. V /\ ( x = A /\ y = A ) ) -> ( x i^i y ) e. { (/) , A } )
64 63 ex
 |-  ( A e. V -> ( ( x = A /\ y = A ) -> ( x i^i y ) e. { (/) , A } ) )
65 46 51 57 64 ccased
 |-  ( A e. V -> ( ( ( x = (/) \/ x = A ) /\ ( y = (/) \/ y = A ) ) -> ( x i^i y ) e. { (/) , A } ) )
66 65 expdimp
 |-  ( ( A e. V /\ ( x = (/) \/ x = A ) ) -> ( ( y = (/) \/ y = A ) -> ( x i^i y ) e. { (/) , A } ) )
67 40 66 syl5bi
 |-  ( ( A e. V /\ ( x = (/) \/ x = A ) ) -> ( y e. { (/) , A } -> ( x i^i y ) e. { (/) , A } ) )
68 67 ralrimiv
 |-  ( ( A e. V /\ ( x = (/) \/ x = A ) ) -> A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } )
69 68 ex
 |-  ( A e. V -> ( ( x = (/) \/ x = A ) -> A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) )
70 38 69 syl5bi
 |-  ( A e. V -> ( x e. { (/) , A } -> A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) )
71 70 ralrimiv
 |-  ( A e. V -> A. x e. { (/) , A } A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } )
72 prex
 |-  { (/) , A } e. _V
73 istopg
 |-  ( { (/) , A } e. _V -> ( { (/) , A } e. Top <-> ( A. x ( x C_ { (/) , A } -> U. x e. { (/) , A } ) /\ A. x e. { (/) , A } A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) ) )
74 72 73 mp1i
 |-  ( A e. V -> ( { (/) , A } e. Top <-> ( A. x ( x C_ { (/) , A } -> U. x e. { (/) , A } ) /\ A. x e. { (/) , A } A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) ) )
75 36 71 74 mpbir2and
 |-  ( A e. V -> { (/) , A } e. Top )
76 28 eqcomd
 |-  ( A e. V -> A = U. { (/) , A } )
77 istopon
 |-  ( { (/) , A } e. ( TopOn ` A ) <-> ( { (/) , A } e. Top /\ A = U. { (/) , A } ) )
78 75 76 77 sylanbrc
 |-  ( A e. V -> { (/) , A } e. ( TopOn ` A ) )