ordunisssuc

Description: A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003)

		Ref	Expression
	Assertion	ordunisssuc	$⊢ (A \subseteq On \land Ord B) \to (⋃ A \subseteq B \leftrightarrow A \subseteq suc B)$

Step	Hyp	Ref	Expression
1		ssel2	$⊢ (A \subseteq On \land x \in A) \to x \in On$
2		ordsssuc	$⊢ (x \in On \land Ord B) \to (x \subseteq B \leftrightarrow x \in suc B)$
3	1 2	sylan	$⊢ ((A \subseteq On \land x \in A) \land Ord B) \to (x \subseteq B \leftrightarrow x \in suc B)$
4	3	an32s	$⊢ ((A \subseteq On \land Ord B) \land x \in A) \to (x \subseteq B \leftrightarrow x \in suc B)$
5	4	ralbidva	$⊢ (A \subseteq On \land Ord B) \to (\forall x \in A x \subseteq B \leftrightarrow \forall x \in A x \in suc B)$
6		unissb	$⊢ ⋃ A \subseteq B \leftrightarrow \forall x \in A x \subseteq B$
7		dfss3	$⊢ A \subseteq suc B \leftrightarrow \forall x \in A x \in suc B$
8	5 6 7	3bitr4g	$⊢ (A \subseteq On \land Ord B) \to (⋃ A \subseteq B \leftrightarrow A \subseteq suc B)$

Metamath Proof Explorer