noinfbnd1lem3

Description: Lemma for noinfbnd1 . If U is a prolongment of T and in B , then ( Udom T ) is not 1o . (Contributed by Scott Fenton, 9-Aug-2024)

		Ref	Expression
	Hypothesis	noinfbnd1.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))))$
	Assertion	noinfbnd1lem3	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land (U \in B \land {U ↾}_{dom T} = T)) \to U (dom T) \neq 1_{𝑜}$

Proof

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

Metamath Proof Explorer

Theorem noinfbnd1lem3

Proof