Theorem etasslt2

Description: A version of etasslt with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021)

	Ref	Expression
Assertion	etasslt2	|- ( A < E. x e. No ( A <

Proof

Step	Hyp	Ref	Expression
1		bdayfun	|- Fun bday
2		ssltex1	|- ( A < A e. _V )
3		ssltex2	|- ( A < B e. _V )
4		unexg	|- ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
5	2 3 4	syl2anc	|- ( A < ( A u. B ) e. _V )
6		funimaexg	|- ( ( Fun bday /\ ( A u. B ) e. _V ) -> ( bday " ( A u. B ) ) e. _V )
7	1 5 6	sylancr	|- ( A < ( bday " ( A u. B ) ) e. _V )
8	7	uniexd	|- ( A < U. ( bday " ( A u. B ) ) e. _V )
9		imassrn	|- ( bday " ( A u. B ) ) C_ ran bday
10		bdayrn	|- ran bday = On
11	9 10	sseqtri	|- ( bday " ( A u. B ) ) C_ On
12		ssorduni	|- ( ( bday " ( A u. B ) ) C_ On -> Ord U. ( bday " ( A u. B ) ) )
13	11 12	ax-mp	|- Ord U. ( bday " ( A u. B ) )
14		elon2	|- ( U. ( bday " ( A u. B ) ) e. On <-> ( Ord U. ( bday " ( A u. B ) ) /\ U. ( bday " ( A u. B ) ) e. _V ) )
15	13 14	mpbiran	|- ( U. ( bday " ( A u. B ) ) e. On <-> U. ( bday " ( A u. B ) ) e. _V )
16	8 15	sylibr	|- ( A < U. ( bday " ( A u. B ) ) e. On )
17		sucelon	|- ( U. ( bday " ( A u. B ) ) e. On <-> suc U. ( bday " ( A u. B ) ) e. On )
18	16 17	sylib	|- ( A < suc U. ( bday " ( A u. B ) ) e. On )
19		onsucuni	|- ( ( bday " ( A u. B ) ) C_ On -> ( bday " ( A u. B ) ) C_ suc U. ( bday " ( A u. B ) ) )
20	11 19	mp1i	|- ( A < ( bday " ( A u. B ) ) C_ suc U. ( bday " ( A u. B ) ) )
21		etasslt	|- ( ( A < E. x e. No ( A <
22	18 20 21	mpd3an23	|- ( A < E. x e. No ( A <