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	|- ( ( A C_ On /\ A e. V ) -> ( ( B C_ A /\ A. a e. A E. b e. B a C_ b ) -> U. A = U. B ) )

Proof

Step	Hyp	Ref	Expression
1		uniss2	|- ( A. a e. A E. b e. B a C_ b -> U. A C_ U. B )
2	1	adantl	|- ( ( B C_ A /\ A. a e. A E. b e. B a C_ b ) -> U. A C_ U. B )
3		uniss	|- ( B C_ A -> U. B C_ U. A )
4	3	adantr	|- ( ( B C_ A /\ A. a e. A E. b e. B a C_ b ) -> U. B C_ U. A )
5	2 4	eqssd	|- ( ( B C_ A /\ A. a e. A E. b e. B a C_ b ) -> U. A = U. B )
6	5	a1i	|- ( ( A C_ On /\ A e. V ) -> ( ( B C_ A /\ A. a e. A E. b e. B a C_ b ) -> U. A = U. B ) )