Theorem 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 \mathrm{On}\to \left(A\notin \mathrm{V}\leftrightarrow \bigcup A=\mathrm{On}\right)$$

Proof

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