nosupbday

Description: Birthday bounding law for surreal supremum. (Contributed by Scott Fenton, 5-Dec-2021)

		Ref	Expression
	Hypothesis	nosupbday.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	Assertion	nosupbday	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to bday (S) \subseteq O$

Proof

Step	Hyp	Ref	Expression
1		nosupbday.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
3	2	adantr	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to S \in No$
4		bdayval	$⊢ S \in No \to bday (S) = dom S$
5	3 4	syl	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to bday (S) = dom S$
6		iftrue	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))) = (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}$
7	1 6	syl5eq	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to S = (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}$
8	7	dmeqd	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = dom ((ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\})$
9		2oex	$⊢ 2_{𝑜} \in V$
10	9	dmsnop	$⊢ dom \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\} = \{dom (ι x \in A \| \forall y \in A \neg x <_{s} y)\}$
11	10	uneq2i	$⊢ dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup dom \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\} = dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{dom (ι x \in A \| \forall y \in A \neg x <_{s} y)\}$
12		dmun	$⊢ dom ((ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}) = dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup dom \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}$
13		df-suc	$⊢ suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) = dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{dom (ι x \in A \| \forall y \in A \neg x <_{s} y)\}$
14	11 12 13	3eqtr4i	$⊢ dom ((ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}) = suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
15	8 14	eqtrdi	$⊢ \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
16	15	adantr	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to dom S = suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
17		simprrl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to O \in On$
18		eloni	$⊢ O \in On \to Ord O$
19	17 18	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to Ord O$
20		simprll	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to A \subseteq No$
21		simpl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to \exists x \in A \forall y \in A \neg x <_{s} y$
22		nomaxmo	$⊢ A \subseteq No \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
23	22	adantr	$⊢ (A \subseteq No \land A \in V) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
24	23	adantl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to \exists^{*} x \in A \forall y \in A \neg x <_{s} y$
25		reu5	$⊢ \exists! x \in A \forall y \in A \neg x <_{s} y \leftrightarrow (\exists x \in A \forall y \in A \neg x <_{s} y \land \exists^{*} x \in A \forall y \in A \neg x <_{s} y)$
26	21 24 25	sylanbrc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V)) \to \exists! x \in A \forall y \in A \neg x <_{s} y$
27	26	adantrr	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to \exists! x \in A \forall y \in A \neg x <_{s} y$
28		riotacl	$⊢ \exists! x \in A \forall y \in A \neg x <_{s} y \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in A$
29	27 28	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in A$
30	20 29	sseldd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No$
31		bdayval	$⊢ (ι x \in A \| \forall y \in A \neg x <_{s} y) \in No \to bday ((ι x \in A \| \forall y \in A \neg x <_{s} y)) = dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
32	30 31	syl	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to bday ((ι x \in A \| \forall y \in A \neg x <_{s} y)) = dom (ι x \in A \| \forall y \in A \neg x <_{s} y)$
33		simprrr	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to bday [A] \subseteq O$
34		bdayfo	$⊢ bday : No \underset{onto}{⟶} On$
35		fofn	$⊢ bday : No \underset{onto}{⟶} On \to bday Fn No$
36	34 35	ax-mp	$⊢ bday Fn No$
37		fnfvima	$⊢ (bday Fn No \land A \subseteq No \land (ι x \in A \| \forall y \in A \neg x <_{s} y) \in A) \to bday ((ι x \in A \| \forall y \in A \neg x <_{s} y)) \in bday [A]$
38	36 20 29 37	mp3an2i	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to bday ((ι x \in A \| \forall y \in A \neg x <_{s} y)) \in bday [A]$
39	33 38	sseldd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to bday ((ι x \in A \| \forall y \in A \neg x <_{s} y)) \in O$
40	32 39	eqeltrrd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in O$
41		ordsucss	$⊢ Ord O \to (dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \in O \to suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \subseteq O)$
42	19 40 41	sylc	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to suc dom (ι x \in A \| \forall y \in A \neg x <_{s} y) \subseteq O$
43	16 42	eqsstrd	$⊢ (\exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to dom S \subseteq O$
44		iffalse	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))) = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
45	1 44	syl5eq	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to S = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
46	45	dmeqd	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = dom (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
47		iotaex	$⊢ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)) \in V$
48		eqid	$⊢ (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
49	47 48	dmmpti	$⊢ dom (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) = \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\}$
50	46 49	eqtrdi	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\}$
51	50	adantr	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to dom S = \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\}$
52		simplrl	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to O \in On$
53		ssel2	$⊢ (A \subseteq No \land u \in A) \to u \in No$
54	53	ad4ant14	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to u \in No$
55		bdayval	$⊢ u \in No \to bday (u) = dom u$
56	54 55	syl	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to bday (u) = dom u$
57		simplrr	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to bday [A] \subseteq O$
58		fnfvima	$⊢ (bday Fn No \land A \subseteq No \land u \in A) \to bday (u) \in bday [A]$
59	36 58	mp3an1	$⊢ (A \subseteq No \land u \in A) \to bday (u) \in bday [A]$
60	59	ad4ant14	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to bday (u) \in bday [A]$
61	57 60	sseldd	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to bday (u) \in O$
62	56 61	eqeltrrd	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to dom u \in O$
63		onelss	$⊢ O \in On \to (dom u \in O \to dom u \subseteq O)$
64	52 62 63	sylc	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to dom u \subseteq O$
65	64	sseld	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to (y \in dom u \to y \in O)$
66	65	adantrd	$⊢ (((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \land u \in A) \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \to y \in O)$
67	66	rexlimdva	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to (\exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \to y \in O)$
68	67	abssdv	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} \subseteq O$
69	68	adantl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} \subseteq O$
70	51 69	eqsstrd	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O))) \to dom S \subseteq O$
71	43 70	pm2.61ian	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to dom S \subseteq O$
72	5 71	eqsstrd	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to bday (S) \subseteq O$

Metamath Proof Explorer

Theorem nosupbday

Proof