ssonprc

Description: Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013)

		Ref	Expression
	Assertion	ssonprc	$⊢ A \subseteq On \to (A \notin V \leftrightarrow ⋃ A = On)$

Step	Hyp	Ref	Expression
1		df-nel	$⊢ A \notin V \leftrightarrow \neg A \in V$
2		ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$
3		ordeleqon	$⊢ Ord ⋃ A \leftrightarrow (⋃ A \in On \lor ⋃ A = On)$
4	2 3	sylib	$⊢ A \subseteq On \to (⋃ A \in On \lor ⋃ A = On)$
5	4	orcomd	$⊢ A \subseteq On \to (⋃ A = On \lor ⋃ A \in On)$
6	5	ord	$⊢ A \subseteq On \to (\neg ⋃ A = On \to ⋃ A \in On)$
7		uniexr	$⊢ ⋃ A \in On \to A \in V$
8	6 7	syl6	$⊢ A \subseteq On \to (\neg ⋃ A = On \to A \in V)$
9	8	con1d	$⊢ A \subseteq On \to (\neg A \in V \to ⋃ A = On)$
10		onprc	$⊢ \neg On \in V$
11		uniexg	$⊢ A \in V \to ⋃ A \in V$
12		eleq1	$⊢ ⋃ A = On \to (⋃ A \in V \leftrightarrow On \in V)$
13	11 12	imbitrid	$⊢ ⋃ A = On \to (A \in V \to On \in V)$
14	10 13	mtoi	$⊢ ⋃ A = On \to \neg A \in V$
15	9 14	impbid1	$⊢ A \subseteq On \to (\neg A \in V \leftrightarrow ⋃ A = On)$
16	1 15	bitrid	$⊢ A \subseteq On \to (A \notin V \leftrightarrow ⋃ A = On)$

Metamath Proof Explorer