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		bdayfo	$⊢ bday : No \underset{onto}{⟶} On$
3		fofun	$⊢ bday : No \underset{onto}{⟶} On \to Fun bday$
4	2 3	ax-mp	$⊢ Fun bday$
5		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$
6		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$
7		unexg	$⊢ (A \in V \land B \in W) \to A \cup B \in V$
8	5 6 7	syl2anc	$⊢ ((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$
9		funimaexg	$⊢ (Fun bday \land A \cup B \in V) \to bday [A \cup B] \in V$
10	4 8 9	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$
11	10	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$
12		imassrn	$⊢ bday [A \cup B] \subseteq ran bday$
13		forn	$⊢ bday : No \underset{onto}{⟶} On \to ran bday = On$
14	2 13	ax-mp	$⊢ ran bday = On$
15	12 14	sseqtri	$⊢ bday [A \cup B] \subseteq On$
16		ssorduni	$⊢ bday [A \cup B] \subseteq On \to Ord ⋃ bday [A \cup B]$
17	15 16	ax-mp	$⊢ Ord ⋃ bday [A \cup B]$
18		elon2	$⊢ ⋃ bday [A \cup B] \in On \leftrightarrow (Ord ⋃ bday [A \cup B] \land ⋃ bday [A \cup B] \in V)$
19	17 18	mpbiran	$⊢ ⋃ bday [A \cup B] \in On \leftrightarrow ⋃ bday [A \cup B] \in V$
20	11 19	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$
21		sucelon	$⊢ ⋃ bday [A \cup B] \in On \leftrightarrow suc ⋃ bday [A \cup B] \in On$
22	20 21	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$
23		onsucuni	$⊢ bday [A \cup B] \subseteq On \to bday [A \cup B] \subseteq suc ⋃ bday [A \cup B]$
24	15 23	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]$
25		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])$
26	1 22 24 25	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