noeta2

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

		Ref	Expression
	Assertion	noeta2	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to \exists z \in No (\forall x \in A x <_{s} z \land \forall y \in B z <_{s} y \land bday (z) \subseteq suc ⋃ bday [A \cup B])$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y)$
2		bdayfun	$⊢ Fun bday$
3		simp1r	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to A \in V$
4		simp2r	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to B \in W$
5	3 4	unexd	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to A \cup B \in V$
6		funimaexg	$⊢ (Fun bday \land A \cup B \in V) \to bday [A \cup B] \in V$
7	2 5 6	sylancr	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to bday [A \cup B] \in V$
8	7	uniexd	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \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 \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to ⋃ bday [A \cup B] \in On$
17		onsucb	$⊢ ⋃ bday [A \cup B] \in On \leftrightarrow suc ⋃ bday [A \cup B] \in On$
18	16 17	sylib	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \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 \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to bday [A \cup B] \subseteq suc ⋃ bday [A \cup B]$
21		noeta	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \land (suc ⋃ bday [A \cup B] \in On \land bday [A \cup B] \subseteq suc ⋃ bday [A \cup B])) \to \exists z \in No (\forall x \in A x <_{s} z \land \forall y \in B z <_{s} y \land bday (z) \subseteq suc ⋃ bday [A \cup B])$
22	1 18 20 21	syl12anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall x \in A \forall y \in B x <_{s} y) \to \exists z \in No (\forall x \in A x <_{s} z \land \forall y \in B z <_{s} y \land bday (z) \subseteq suc ⋃ bday [A \cup B])$

Metamath Proof Explorer

Theorem noeta2

Proof