noetainflem3

Description: Lemma for noeta . W bounds B below . (Contributed by Scott Fenton, 9-Aug-2024)

	Ref	Expression
Hypotheses	noetainflem.1	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	noetainflem.2	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
Assertion	noetainflem3	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to W <_{s} Y$

Proof

Step	Hyp	Ref	Expression
1		noetainflem.1	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		noetainflem.2	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
3		simpl2	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to B \subseteq No$
4		simpl3	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to B \in V$
5	1 2	noetainflem2	$⊢ (B \subseteq No \land B \in V) \to {W ↾}_{dom T} = T$
6	3 4 5	syl2anc	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to {W ↾}_{dom T} = T$
7		simpr	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to Y \in B$
8	1	noinfbnd1	$⊢ (B \subseteq No \land B \in V \land Y \in B) \to T <_{s} ({Y ↾}_{dom T})$
9	3 4 7 8	syl3anc	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to T <_{s} ({Y ↾}_{dom T})$
10	6 9	eqbrtrd	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to ({W ↾}_{dom T}) <_{s} ({Y ↾}_{dom T})$
11	1 2	noetainflem1	$⊢ (A \in V \land B \subseteq No \land B \in V) \to W \in No$
12	11	adantr	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to W \in No$
13		simp2	$⊢ (A \in V \land B \subseteq No \land B \in V) \to B \subseteq No$
14	13	sselda	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to Y \in No$
15	1	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
16	3 4 15	syl2anc	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to T \in No$
17		nodmon	$⊢ T \in No \to dom T \in On$
18	16 17	syl	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to dom T \in On$
19		sltres	$⊢ (W \in No \land Y \in No \land dom T \in On) \to (({W ↾}_{dom T}) <_{s} ({Y ↾}_{dom T}) \to W <_{s} Y)$
20	12 14 18 19	syl3anc	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to (({W ↾}_{dom T}) <_{s} ({Y ↾}_{dom T}) \to W <_{s} Y)$
21	10 20	mpd	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land Y \in B) \to W <_{s} Y$

Metamath Proof Explorer

Theorem noetainflem3

Proof