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