nosupbnd1lem2

Description: Lemma for nosupbnd1 . When there is no maximum, if any member of A is a prolongment of S , then so are all elements of A above it. (Contributed by Scott Fenton, 5-Dec-2021)

		Ref	Expression
	Hypothesis	nosupbnd1.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	nosupbnd1lem2	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to {W ↾}_{dom S} = S$

Proof

Step	Hyp	Ref	Expression
1		nosupbnd1.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		simp3rr	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to \neg W <_{s} U$
3		simp2l	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to A \subseteq No$
4		simp3rl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to W \in A$
5	3 4	sseldd	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to W \in No$
6		simp3ll	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to U \in A$
7	3 6	sseldd	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to U \in No$
8	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
9	8	3ad2ant2	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to S \in No$
10		nodmon	$⊢ S \in No \to dom S \in On$
11	9 10	syl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to dom S \in On$
12		ltsres	$⊢ (W \in No \land U \in No \land dom S \in On) \to (({W ↾}_{dom S}) <_{s} ({U ↾}_{dom S}) \to W <_{s} U)$
13	5 7 11 12	syl3anc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to (({W ↾}_{dom S}) <_{s} ({U ↾}_{dom S}) \to W <_{s} U)$
14	2 13	mtod	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to \neg ({W ↾}_{dom S}) <_{s} ({U ↾}_{dom S})$
15		simp3lr	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to {U ↾}_{dom S} = S$
16	15	breq2d	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to (({W ↾}_{dom S}) <_{s} ({U ↾}_{dom S}) \leftrightarrow ({W ↾}_{dom S}) <_{s} S)$
17	14 16	mtbid	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to \neg ({W ↾}_{dom S}) <_{s} S$
18	1	nosupbnd1lem1	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land W \in A) \to \neg S <_{s} ({W ↾}_{dom S})$
19	4 18	syld3an3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to \neg S <_{s} ({W ↾}_{dom S})$
20		noreson	$⊢ (W \in No \land dom S \in On) \to {W ↾}_{dom S} \in No$
21	5 11 20	syl2anc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to {W ↾}_{dom S} \in No$
22		ltsso	$⊢ <_{s} Or No$
23		sotrieq2	$⊢ (<_{s} Or No \land ({W ↾}_{dom S} \in No \land S \in No)) \to ({W ↾}_{dom S} = S \leftrightarrow (\neg ({W ↾}_{dom S}) <_{s} S \land \neg S <_{s} ({W ↾}_{dom S})))$
24	22 23	mpan	$⊢ ({W ↾}_{dom S} \in No \land S \in No) \to ({W ↾}_{dom S} = S \leftrightarrow (\neg ({W ↾}_{dom S}) <_{s} S \land \neg S <_{s} ({W ↾}_{dom S})))$
25	21 9 24	syl2anc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to ({W ↾}_{dom S} = S \leftrightarrow (\neg ({W ↾}_{dom S}) <_{s} S \land \neg S <_{s} ({W ↾}_{dom S})))$
26	17 19 25	mpbir2and	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land ((U \in A \land {U ↾}_{dom S} = S) \land (W \in A \land \neg W <_{s} U))) \to {W ↾}_{dom S} = S$

Metamath Proof Explorer

Theorem nosupbnd1lem2

Proof