noetasuplem3

Description: Lemma for noeta . Z is an upper bound for A . Part of Theorem 5.1 of Lipparini p. 7-8. (Contributed by Scott Fenton, 4-Dec-2021)

	Ref	Expression
Hypotheses	noetasuplem.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))))$
	noetasuplem.2	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
Assertion	noetasuplem3	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to X <_{s} Z$

Proof

Step	Hyp	Ref	Expression
1		noetasuplem.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		noetasuplem.2	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
3		simpl1	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to A \subseteq No$
4		simpl2	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to A \in V$
5		simpr	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to X \in A$
6	1	nosupbnd1	$⊢ (A \subseteq No \land A \in V \land X \in A) \to ({X ↾}_{dom S}) <_{s} S$
7	3 4 5 6	syl3anc	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to ({X ↾}_{dom S}) <_{s} S$
8	2	reseq1i	$⊢ {Z ↾}_{dom S} = {(S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) ↾}_{dom S}$
9		resundir	$⊢ {(S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) ↾}_{dom S} = ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S})$
10		df-res	$⊢ {((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S} = ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V)$
11		incom	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = dom S \cap (suc ⋃ bday [B] ∖ dom S)$
12		disjdif	$⊢ dom S \cap (suc ⋃ bday [B] ∖ dom S) = \emptyset$
13	11 12	eqtri	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset$
14		xpdisj1	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
15	13 14	ax-mp	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
16	10 15	eqtri	$⊢ {((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S} = \emptyset$
17	16	uneq2i	$⊢ ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S}) = ({S ↾}_{dom S}) \cup \emptyset$
18		un0	$⊢ ({S ↾}_{dom S}) \cup \emptyset = {S ↾}_{dom S}$
19	9 17 18	3eqtri	$⊢ {(S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) ↾}_{dom S} = {S ↾}_{dom S}$
20	8 19	eqtri	$⊢ {Z ↾}_{dom S} = {S ↾}_{dom S}$
21	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
22	3 4 21	syl2anc	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to S \in No$
23		nofun	$⊢ S \in No \to Fun S$
24	22 23	syl	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to Fun S$
25		funrel	$⊢ Fun S \to Rel S$
26		resdm	$⊢ Rel S \to {S ↾}_{dom S} = S$
27	24 25 26	3syl	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to {S ↾}_{dom S} = S$
28	20 27	syl5eq	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to {Z ↾}_{dom S} = S$
29	7 28	breqtrrd	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to ({X ↾}_{dom S}) <_{s} ({Z ↾}_{dom S})$
30		simp1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to A \subseteq No$
31	30	sselda	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to X \in No$
32	1 2	noetasuplem1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to Z \in No$
33	32	adantr	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to Z \in No$
34		nodmon	$⊢ S \in No \to dom S \in On$
35	22 34	syl	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to dom S \in On$
36		sltres	$⊢ (X \in No \land Z \in No \land dom S \in On) \to (({X ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}) \to X <_{s} Z)$
37	31 33 35 36	syl3anc	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to (({X ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}) \to X <_{s} Z)$
38	29 37	mpd	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to X <_{s} Z$

Metamath Proof Explorer

Theorem noetasuplem3

Proof