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 ) )