cutbdaybnd2lim

Description: An upper bound on the birthday of a surreal cut when it is a limit birthday. (Contributed by Scott Fenton, 7-Aug-2024)

		Ref	Expression
	Assertion	cutbdaybnd2lim	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to bday (A \|_{s} B) \subseteq ⋃ bday [A \cup B]$

Proof

Step	Hyp	Ref	Expression
1		cutbdaybnd2	$⊢ A ≪_{s} B \to bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B]$
2	1	adantr	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B]$
3		bdayfun	$⊢ Fun bday$
4		sltsex1	$⊢ A ≪_{s} B \to A \in V$
5		sltsex2	$⊢ A ≪_{s} B \to B \in V$
6		unexg	$⊢ (A \in V \land B \in V) \to A \cup B \in V$
7	4 5 6	syl2anc	$⊢ A ≪_{s} B \to A \cup B \in V$
8		funimaexg	$⊢ (Fun bday \land A \cup B \in V) \to bday [A \cup B] \in V$
9	3 7 8	sylancr	$⊢ A ≪_{s} B \to bday [A \cup B] \in V$
10	9	uniexd	$⊢ A ≪_{s} B \to ⋃ bday [A \cup B] \in V$
11	10	adantr	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to ⋃ bday [A \cup B] \in V$
12		nlimsucg	$⊢ ⋃ bday [A \cup B] \in V \to \neg Lim suc ⋃ bday [A \cup B]$
13	11 12	syl	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to \neg Lim suc ⋃ bday [A \cup B]$
14		limeq	$⊢ bday (A \|_{s} B) = suc ⋃ bday [A \cup B] \to (Lim bday (A \|_{s} B) \leftrightarrow Lim suc ⋃ bday [A \cup B])$
15	14	biimpcd	$⊢ Lim bday (A \|_{s} B) \to (bday (A \|_{s} B) = suc ⋃ bday [A \cup B] \to Lim suc ⋃ bday [A \cup B])$
16	15	adantl	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to (bday (A \|_{s} B) = suc ⋃ bday [A \cup B] \to Lim suc ⋃ bday [A \cup B])$
17	13 16	mtod	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to \neg bday (A \|_{s} B) = suc ⋃ bday [A \cup B]$
18	17	neqned	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to bday (A \|_{s} B) \neq suc ⋃ bday [A \cup B]$
19		bdayon	$⊢ bday (A \|_{s} B) \in On$
20	19	onordi	$⊢ Ord bday (A \|_{s} B)$
21		imassrn	$⊢ bday [A \cup B] \subseteq ran bday$
22		bdayrn	$⊢ ran bday = On$
23	21 22	sseqtri	$⊢ bday [A \cup B] \subseteq On$
24		ssorduni	$⊢ bday [A \cup B] \subseteq On \to Ord ⋃ bday [A \cup B]$
25	23 24	ax-mp	$⊢ Ord ⋃ bday [A \cup B]$
26		ordsuc	$⊢ Ord ⋃ bday [A \cup B] \leftrightarrow Ord suc ⋃ bday [A \cup B]$
27	25 26	mpbi	$⊢ Ord suc ⋃ bday [A \cup B]$
28		ordelssne	$⊢ (Ord bday (A \|_{s} B) \land Ord suc ⋃ bday [A \cup B]) \to (bday (A \|_{s} B) \in suc ⋃ bday [A \cup B] \leftrightarrow (bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B] \land bday (A \|_{s} B) \neq suc ⋃ bday [A \cup B]))$
29	20 27 28	mp2an	$⊢ bday (A \|_{s} B) \in suc ⋃ bday [A \cup B] \leftrightarrow (bday (A \|_{s} B) \subseteq suc ⋃ bday [A \cup B] \land bday (A \|_{s} B) \neq suc ⋃ bday [A \cup B])$
30	2 18 29	sylanbrc	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to bday (A \|_{s} B) \in suc ⋃ bday [A \cup B]$
31	19	a1i	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to bday (A \|_{s} B) \in On$
32		ordsssuc	$⊢ (bday (A \|_{s} B) \in On \land Ord ⋃ bday [A \cup B]) \to (bday (A \|_{s} B) \subseteq ⋃ bday [A \cup B] \leftrightarrow bday (A \|_{s} B) \in suc ⋃ bday [A \cup B])$
33	31 25 32	sylancl	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to (bday (A \|_{s} B) \subseteq ⋃ bday [A \cup B] \leftrightarrow bday (A \|_{s} B) \in suc ⋃ bday [A \cup B])$
34	30 33	mpbird	$⊢ (A ≪_{s} B \land Lim bday (A \|_{s} B)) \to bday (A \|_{s} B) \subseteq ⋃ bday [A \cup B]$

Metamath Proof Explorer

Theorem cutbdaybnd2lim

Proof