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 ≪_{s} B \to \exists x \in No (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B])$

Proof

Step	Hyp	Ref	Expression
1		bdayfun	$⊢ Fun bday$
2		ssltex1	$⊢ A ≪_{s} B \to A \in V$
3		ssltex2	$⊢ A ≪_{s} B \to B \in V$
4		unexg	$⊢ (A \in V \land B \in V) \to A \cup B \in V$
5	2 3 4	syl2anc	$⊢ A ≪_{s} B \to A \cup B \in V$
6		funimaexg	$⊢ (Fun bday \land A \cup B \in V) \to bday [A \cup B] \in V$
7	1 5 6	sylancr	$⊢ A ≪_{s} B \to bday [A \cup B] \in V$
8	7	uniexd	$⊢ A ≪_{s} B \to ⋃ bday [A \cup B] \in V$
9		imassrn	$⊢ bday [A \cup B] \subseteq ran bday$
10		bdayrn	$⊢ ran bday = On$
11	9 10	sseqtri	$⊢ bday [A \cup B] \subseteq On$
12		ssorduni	$⊢ bday [A \cup B] \subseteq On \to Ord ⋃ bday [A \cup B]$
13	11 12	ax-mp	$⊢ Ord ⋃ bday [A \cup B]$
14		elon2	$⊢ ⋃ bday [A \cup B] \in On \leftrightarrow (Ord ⋃ bday [A \cup B] \land ⋃ bday [A \cup B] \in V)$
15	13 14	mpbiran	$⊢ ⋃ bday [A \cup B] \in On \leftrightarrow ⋃ bday [A \cup B] \in V$
16	8 15	sylibr	$⊢ A ≪_{s} B \to ⋃ bday [A \cup B] \in On$
17		sucelon	$⊢ ⋃ bday [A \cup B] \in On \leftrightarrow suc ⋃ bday [A \cup B] \in On$
18	16 17	sylib	$⊢ A ≪_{s} B \to suc ⋃ bday [A \cup B] \in On$
19		onsucuni	$⊢ bday [A \cup B] \subseteq On \to bday [A \cup B] \subseteq suc ⋃ bday [A \cup B]$
20	11 19	mp1i	$⊢ A ≪_{s} B \to bday [A \cup B] \subseteq suc ⋃ bday [A \cup B]$
21		etasslt	$⊢ (A ≪_{s} B \land suc ⋃ bday [A \cup B] \in On \land bday [A \cup B] \subseteq suc ⋃ bday [A \cup B]) \to \exists x \in No (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B])$
22	18 20 21	mpd3an23	$⊢ A ≪_{s} B \to \exists x \in No (A ≪_{s} \{x\} \land \{x\} ≪_{s} B \land bday (x) \subseteq suc ⋃ bday [A \cup B])$

Metamath Proof Explorer

Theorem etasslt2

Proof