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	⊢ ( 𝐴 <<s 𝐵 → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bdayfun	⊢ Fun bday
2		ssltex1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
3		ssltex2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
4		unexg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
5	2 3 4	syl2anc	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 ∪ 𝐵 ) ∈ V )
6		funimaexg	⊢ ( ( Fun bday ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
7	1 5 6	sylancr	⊢ ( 𝐴 <<s 𝐵 → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
8	7	uniexd	⊢ ( 𝐴 <<s 𝐵 → ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
9		imassrn	⊢ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ ran bday
10		bdayrn	⊢ ran bday = On
11	9 10	sseqtri	⊢ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On
12		ssorduni	⊢ ( ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On → Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
13	11 12	ax-mp	⊢ Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) )
14		elon2	⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ ( Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∧ ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V ) )
15	13 14	mpbiran	⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
16	8 15	sylibr	⊢ ( 𝐴 <<s 𝐵 → ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
17		sucelon	⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
18	16 17	sylib	⊢ ( 𝐴 <<s 𝐵 → suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
19		onsucuni	⊢ ( ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
20	11 19	mp1i	⊢ ( 𝐴 <<s 𝐵 → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
21		etasslt	⊢ ( ( 𝐴 <<s 𝐵 ∧ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )
22	18 20 21	mpd3an23	⊢ ( 𝐴 <<s 𝐵 → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )