Theorem onsssupeqcond

Description: If for every element of a set of ordinals there is an element of a subset which is at least as large, then the union of the set and the subset is the same. Lemma 2.12 of Schloeder p. 5. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsssupeqcond	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \left(\left(B\subseteq A\wedge \forall a\in A\exists b\in Ba\subseteq b\right)\to \bigcup A=\bigcup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		uniss2	$$⊢\forall a\in A\exists b\in Ba\subseteq b\to \bigcup A\subseteq \bigcup B$$
2	1	adantl	$$⊢\left(B\subseteq A\wedge \forall a\in A\exists b\in Ba\subseteq b\right)\to \bigcup A\subseteq \bigcup B$$
3		uniss	$$⊢B\subseteq A\to \bigcup B\subseteq \bigcup A$$
4	3	adantr	$$⊢\left(B\subseteq A\wedge \forall a\in A\exists b\in Ba\subseteq b\right)\to \bigcup B\subseteq \bigcup A$$
5	2 4	eqssd	$$⊢\left(B\subseteq A\wedge \forall a\in A\exists b\in Ba\subseteq b\right)\to \bigcup A=\bigcup B$$
6	5	a1i	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \left(\left(B\subseteq A\wedge \forall a\in A\exists b\in Ba\subseteq b\right)\to \bigcup A=\bigcup B\right)$$