This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ⊆ { ∅ , 𝐴 } → ∪ 𝑥 ∈ { ∅ , 𝐴 } ) )
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 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) → ( 𝑦 ∈ { ∅ , 𝐴 } → ( 𝑥 ∩ 𝑦 ) ∈ { ∅ , 𝐴 } ) )
68 67 ralrimiv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) → ∀ 𝑦 ∈ { ∅ , 𝐴 } ( 𝑥 ∩ 𝑦 ) ∈ { ∅ , 𝐴 } )
69 68 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) → ∀ 𝑦 ∈ { ∅ , 𝐴 } ( 𝑥 ∩ 𝑦 ) ∈ { ∅ , 𝐴 } ) )
70 38 69 biimtrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ { ∅ , 𝐴 } → ∀ 𝑦 ∈ { ∅ , 𝐴 } ( 𝑥 ∩ 𝑦 ) ∈ { ∅ , 𝐴 } ) )
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 ‘ 𝐴 ) )