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 \in V \to \{\emptyset, A\} \in TopOn (A)$

Proof

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

Metamath Proof Explorer

Theorem indistopon

Proof