nosupbnd1lem3

Description: Lemma for nosupbnd1 . If U is a prolongment of S and in A , then ( Udom S ) is not 2o . (Contributed by Scott Fenton, 6-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	nosupbnd1lem3	$⊢ (\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)) \to U (dom S) \neq 2_{𝑜}$

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	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
3	2	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)) \to S \in No$
4		nodmord	$⊢ S \in No \to Ord dom S$
5		ordirr	$⊢ Ord dom S \to \neg dom S \in dom S$
6	3 4 5	3syl	$⊢ (\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)) \to \neg dom S \in dom S$
7		simpl3l	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to U \in A$
8		ndmfv	$⊢ \neg dom S \in dom U \to U (dom S) = \emptyset$
9		2on	$⊢ 2_{𝑜} \in On$
10	9	elexi	$⊢ 2_{𝑜} \in V$
11	10	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
12	11	nosgnn0i	$⊢ \emptyset \neq 2_{𝑜}$
13		neeq1	$⊢ U (dom S) = \emptyset \to (U (dom S) \neq 2_{𝑜} \leftrightarrow \emptyset \neq 2_{𝑜})$
14	12 13	mpbiri	$⊢ U (dom S) = \emptyset \to U (dom S) \neq 2_{𝑜}$
15	14	neneqd	$⊢ U (dom S) = \emptyset \to \neg U (dom S) = 2_{𝑜}$
16	8 15	syl	$⊢ \neg dom S \in dom U \to \neg U (dom S) = 2_{𝑜}$
17	16	con4i	$⊢ U (dom S) = 2_{𝑜} \to dom S \in dom U$
18	17	adantl	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to dom S \in dom U$
19		simpl2l	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to A \subseteq No$
20	19	adantr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to A \subseteq No$
21	7	adantr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to U \in A$
22	20 21	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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to U \in No$
23		simprl	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to q \in A$
24	20 23	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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to q \in No$
25	3	adantr	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to S \in No$
26	25	adantr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to S \in No$
27		nodmon	$⊢ S \in No \to dom S \in On$
28	26 27	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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to dom S \in On$
29		simpl3r	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to {U ↾}_{dom S} = S$
30	29	adantr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to {U ↾}_{dom S} = S$
31		simpll1	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
32		simpll2	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to (A \subseteq No \land A \in V)$
33		simpll3	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to (U \in A \land {U ↾}_{dom S} = S)$
34		simpr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to (q \in A \land \neg q <_{s} U)$
35	1	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 (q \in A \land \neg q <_{s} U))) \to {q ↾}_{dom S} = S$
36	31 32 33 34 35	syl112anc	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to {q ↾}_{dom S} = S$
37	30 36	eqtr4d	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to {U ↾}_{dom S} = {q ↾}_{dom S}$
38		simplr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to U (dom S) = 2_{𝑜}$
39		simprr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to \neg q <_{s} U$
40		nolesgn2ores	$⊢ ((U \in No \land q \in No \land dom S \in On) \land ({U ↾}_{dom S} = {q ↾}_{dom S} \land U (dom S) = 2_{𝑜}) \land \neg q <_{s} U) \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S}$
41	22 24 28 37 38 39 40	syl321anc	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land (q \in A \land \neg q <_{s} U)) \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S}$
42	41	expr	$⊢ (((\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 U (dom S) = 2_{𝑜}) \land q \in A) \to (\neg q <_{s} U \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S})$
43	42	ralrimiva	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to \forall q \in A (\neg q <_{s} U \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S})$
44		dmeq	$⊢ p = U \to dom p = dom U$
45	44	eleq2d	$⊢ p = U \to (dom S \in dom p \leftrightarrow dom S \in dom U)$
46		breq2	$⊢ p = U \to (q <_{s} p \leftrightarrow q <_{s} U)$
47	46	notbid	$⊢ p = U \to (\neg q <_{s} p \leftrightarrow \neg q <_{s} U)$
48		reseq1	$⊢ p = U \to {p ↾}_{suc dom S} = {U ↾}_{suc dom S}$
49	48	eqeq1d	$⊢ p = U \to ({p ↾}_{suc dom S} = {q ↾}_{suc dom S} \leftrightarrow {U ↾}_{suc dom S} = {q ↾}_{suc dom S})$
50	47 49	imbi12d	$⊢ p = U \to ((\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S}) \leftrightarrow (\neg q <_{s} U \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S}))$
51	50	ralbidv	$⊢ p = U \to (\forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S}) \leftrightarrow \forall q \in A (\neg q <_{s} U \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S}))$
52	45 51	anbi12d	$⊢ p = U \to ((dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S})) \leftrightarrow (dom S \in dom U \land \forall q \in A (\neg q <_{s} U \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S})))$
53	52	rspcev	$⊢ (U \in A \land (dom S \in dom U \land \forall q \in A (\neg q <_{s} U \to {U ↾}_{suc dom S} = {q ↾}_{suc dom S}))) \to \exists p \in A (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S}))$
54	7 18 43 53	syl12anc	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to \exists p \in A (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S}))$
55	1	nosupdm	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{z \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\}$
56	55	eleq2d	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to (dom S \in dom S \leftrightarrow dom S \in \{z \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\})$
57	56	3ad2ant1	$⊢ (\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)) \to (dom S \in dom S \leftrightarrow dom S \in \{z \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\})$
58		eleq1	$⊢ z = dom S \to (z \in dom p \leftrightarrow dom S \in dom p)$
59		suceq	$⊢ z = dom S \to suc z = suc dom S$
60	59	reseq2d	$⊢ z = dom S \to {p ↾}_{suc z} = {p ↾}_{suc dom S}$
61	59	reseq2d	$⊢ z = dom S \to {q ↾}_{suc z} = {q ↾}_{suc dom S}$
62	60 61	eqeq12d	$⊢ z = dom S \to ({p ↾}_{suc z} = {q ↾}_{suc z} \leftrightarrow {p ↾}_{suc dom S} = {q ↾}_{suc dom S})$
63	62	imbi2d	$⊢ z = dom S \to ((\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}) \leftrightarrow (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S}))$
64	63	ralbidv	$⊢ z = dom S \to (\forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}) \leftrightarrow \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S}))$
65	58 64	anbi12d	$⊢ z = dom S \to ((z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z})) \leftrightarrow (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S})))$
66	65	rexbidv	$⊢ z = dom S \to (\exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z})) \leftrightarrow \exists p \in A (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S})))$
67	66	elabg	$⊢ dom S \in On \to (dom S \in \{z \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\} \leftrightarrow \exists p \in A (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S})))$
68	3 27 67	3syl	$⊢ (\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)) \to (dom S \in \{z \| \exists p \in A (z \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc z} = {q ↾}_{suc z}))\} \leftrightarrow \exists p \in A (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S})))$
69	57 68	bitrd	$⊢ (\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)) \to (dom S \in dom S \leftrightarrow \exists p \in A (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S})))$
70	69	adantr	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to (dom S \in dom S \leftrightarrow \exists p \in A (dom S \in dom p \land \forall q \in A (\neg q <_{s} p \to {p ↾}_{suc dom S} = {q ↾}_{suc dom S})))$
71	54 70	mpbird	$⊢ ((\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 U (dom S) = 2_{𝑜}) \to dom S \in dom S$
72	6 71	mtand	$⊢ (\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)) \to \neg U (dom S) = 2_{𝑜}$
73	72	neqned	$⊢ (\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)) \to U (dom S) \neq 2_{𝑜}$

Metamath Proof Explorer

Theorem nosupbnd1lem3

Proof