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		disjdifr	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset$
12		xpdisj1	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
13	11 12	ax-mp	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
14	10 13	eqtri	$⊢ {((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S} = \emptyset$
15	14	uneq2i	$⊢ ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S}) = ({S ↾}_{dom S}) \cup \emptyset$
16		un0	$⊢ ({S ↾}_{dom S}) \cup \emptyset = {S ↾}_{dom S}$
17	9 15 16	3eqtri	$⊢ {(S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) ↾}_{dom S} = {S ↾}_{dom S}$
18	8 17	eqtri	$⊢ {Z ↾}_{dom S} = {S ↾}_{dom S}$
19	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
20	3 4 19	syl2anc	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to S \in No$
21		nofun	$⊢ S \in No \to Fun S$
22		funrel	$⊢ Fun S \to Rel S$
23		resdm	$⊢ Rel S \to {S ↾}_{dom S} = S$
24	20 21 22 23	4syl	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to {S ↾}_{dom S} = S$
25	18 24	eqtrid	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to {Z ↾}_{dom S} = S$
26	7 25	breqtrrd	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to ({X ↾}_{dom S}) <_{s} ({Z ↾}_{dom S})$
27		simp1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to A \subseteq No$
28	27	sselda	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to X \in No$
29	1 2	noetasuplem1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to Z \in No$
30	29	adantr	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to Z \in No$
31		nodmon	$⊢ S \in No \to dom S \in On$
32	20 31	syl	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land X \in A) \to dom S \in On$
33		ltsres	$⊢ (X \in No \land Z \in No \land dom S \in On) \to (({X ↾}_{dom S}) <_{s} ({Z ↾}_{dom S}) \to X <_{s} Z)$
34	28 30 32 33	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)$
35	26 34	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