ontgval

Description: The topology generated from an ordinal number B is suc U. B . (Contributed by Chen-Pang He, 10-Oct-2015)

		Ref	Expression
	Assertion	ontgval	$⊢ B \in On \to topGen (B) = suc ⋃ B$

Proof

Step	Hyp	Ref	Expression
1		eltg4i	$⊢ x \in topGen (B) \to x = ⋃ (B \cap 𝒫 x)$
2		inex1g	$⊢ B \in On \to B \cap 𝒫 x \in V$
3		onss	$⊢ B \in On \to B \subseteq On$
4		ssinss1	$⊢ B \subseteq On \to B \cap 𝒫 x \subseteq On$
5	3 4	syl	$⊢ B \in On \to B \cap 𝒫 x \subseteq On$
6		ssonuni	$⊢ B \cap 𝒫 x \in V \to (B \cap 𝒫 x \subseteq On \to ⋃ (B \cap 𝒫 x) \in On)$
7	2 5 6	sylc	$⊢ B \in On \to ⋃ (B \cap 𝒫 x) \in On$
8		eleq1	$⊢ x = ⋃ (B \cap 𝒫 x) \to (x \in On \leftrightarrow ⋃ (B \cap 𝒫 x) \in On)$
9	8	biimprd	$⊢ x = ⋃ (B \cap 𝒫 x) \to (⋃ (B \cap 𝒫 x) \in On \to x \in On)$
10	1 7 9	syl2imc	$⊢ B \in On \to (x \in topGen (B) \to x \in On)$
11		onuni	$⊢ B \in On \to ⋃ B \in On$
12		onsuc	$⊢ ⋃ B \in On \to suc ⋃ B \in On$
13	11 12	syl	$⊢ B \in On \to suc ⋃ B \in On$
14	10 13	jctird	$⊢ B \in On \to (x \in topGen (B) \to (x \in On \land suc ⋃ B \in On))$
15		tg1	$⊢ x \in topGen (B) \to x \subseteq ⋃ B$
16	15	a1i	$⊢ B \in On \to (x \in topGen (B) \to x \subseteq ⋃ B)$
17		sucidg	$⊢ ⋃ B \in On \to ⋃ B \in suc ⋃ B$
18	11 17	syl	$⊢ B \in On \to ⋃ B \in suc ⋃ B$
19	16 18	jctird	$⊢ B \in On \to (x \in topGen (B) \to (x \subseteq ⋃ B \land ⋃ B \in suc ⋃ B))$
20		ontr2	$⊢ (x \in On \land suc ⋃ B \in On) \to ((x \subseteq ⋃ B \land ⋃ B \in suc ⋃ B) \to x \in suc ⋃ B)$
21	14 19 20	syl6c	$⊢ B \in On \to (x \in topGen (B) \to x \in suc ⋃ B)$
22		elsuci	$⊢ x \in suc ⋃ B \to (x \in ⋃ B \lor x = ⋃ B)$
23		eloni	$⊢ B \in On \to Ord B$
24		orduniss	$⊢ Ord B \to ⋃ B \subseteq B$
25	23 24	syl	$⊢ B \in On \to ⋃ B \subseteq B$
26		bastg	$⊢ B \in On \to B \subseteq topGen (B)$
27	25 26	sstrd	$⊢ B \in On \to ⋃ B \subseteq topGen (B)$
28	27	sseld	$⊢ B \in On \to (x \in ⋃ B \to x \in topGen (B))$
29		ssid	$⊢ B \subseteq B$
30		eltg3i	$⊢ (B \in On \land B \subseteq B) \to ⋃ B \in topGen (B)$
31	29 30	mpan2	$⊢ B \in On \to ⋃ B \in topGen (B)$
32		eleq1a	$⊢ ⋃ B \in topGen (B) \to (x = ⋃ B \to x \in topGen (B))$
33	31 32	syl	$⊢ B \in On \to (x = ⋃ B \to x \in topGen (B))$
34	28 33	jaod	$⊢ B \in On \to ((x \in ⋃ B \lor x = ⋃ B) \to x \in topGen (B))$
35	22 34	syl5	$⊢ B \in On \to (x \in suc ⋃ B \to x \in topGen (B))$
36	21 35	impbid	$⊢ B \in On \to (x \in topGen (B) \leftrightarrow x \in suc ⋃ B)$
37	36	eqrdv	$⊢ B \in On \to topGen (B) = suc ⋃ B$

Metamath Proof Explorer

Theorem ontgval

Proof