# 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 ( 𝐴𝑉 → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )

### Proof

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