noinfbnd1lem5

Description: Lemma for noinfbnd1 . If U is a prolongment of T and in B , then ( Udom T ) is not 2o . (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	noinfbnd1lem5	$⊢ (\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 2_{𝑜}$

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	3	adantl	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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$
5		nodmord	$⊢ T \in No \to Ord dom T$
6	4 5	syl	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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 Ord dom T$
7		ordirr	$⊢ Ord dom T \to \neg dom T \in dom T$
8	6 7	syl	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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$
9		simpr3l	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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 \in B$
10	9	adantr	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to U \in B$
11		ndmfv	$⊢ \neg dom T \in dom U \to U (dom T) = \emptyset$
12		2on0	$⊢ 2_{𝑜} \neq \emptyset$
13	12	necomi	$⊢ \emptyset \neq 2_{𝑜}$
14		neeq1	$⊢ U (dom T) = \emptyset \to (U (dom T) \neq 2_{𝑜} \leftrightarrow \emptyset \neq 2_{𝑜})$
15	13 14	mpbiri	$⊢ U (dom T) = \emptyset \to U (dom T) \neq 2_{𝑜}$
16	11 15	syl	$⊢ \neg dom T \in dom U \to U (dom T) \neq 2_{𝑜}$
17	16	neneqd	$⊢ \neg dom T \in dom U \to \neg U (dom T) = 2_{𝑜}$
18	17	con4i	$⊢ U (dom T) = 2_{𝑜} \to dom T \in dom U$
19	18	adantl	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to dom T \in dom U$
20		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) = 2_{𝑜}) \to B \subseteq No$
21	20	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to B \subseteq No$
22		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) = 2_{𝑜}) \to U \in B$
23	22	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to U \in B$
24	21 23	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to U \in No$
25		nofun	$⊢ U \in No \to Fun U$
26	24 25	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to Fun U$
27		simprll	$⊢ (((\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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to z \in B$
28	21 27	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to z \in No$
29		nofun	$⊢ z \in No \to Fun z$
30	28 29	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to Fun z$
31		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) = 2_{𝑜}) \to {U ↾}_{dom T} = T$
32	31	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to {U ↾}_{dom T} = T$
33		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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to \neg \exists x \in B \forall y \in B \neg y <_{s} x$
34		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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to (B \subseteq No \land B \in V)$
35		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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to (U \in B \land {U ↾}_{dom T} = T)$
36		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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to (z \in B \land \neg U <_{s} z)$
37	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 (z \in B \land \neg U <_{s} z))) \to {z ↾}_{dom T} = T$
38	33 34 35 36 37	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to {z ↾}_{dom T} = T$
39	32 38	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to {U ↾}_{dom T} = {z ↾}_{dom T}$
40		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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to U (dom T) = 2_{𝑜}$
41	40 18	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to dom T \in dom U$
42		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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to z (dom T) = 2_{𝑜}$
43		ndmfv	$⊢ \neg dom T \in dom z \to z (dom T) = \emptyset$
44		neeq1	$⊢ z (dom T) = \emptyset \to (z (dom T) \neq 2_{𝑜} \leftrightarrow \emptyset \neq 2_{𝑜})$
45	13 44	mpbiri	$⊢ z (dom T) = \emptyset \to z (dom T) \neq 2_{𝑜}$
46	43 45	syl	$⊢ \neg dom T \in dom z \to z (dom T) \neq 2_{𝑜}$
47	46	neneqd	$⊢ \neg dom T \in dom z \to \neg z (dom T) = 2_{𝑜}$
48	47	con4i	$⊢ z (dom T) = 2_{𝑜} \to dom T \in dom z$
49	42 48	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to dom T \in dom z$
50	40 42	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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to U (dom T) = z (dom T)$
51		eqfunressuc	$⊢ ((Fun U \land Fun z) \land {U ↾}_{dom T} = {z ↾}_{dom T} \land (dom T \in dom U \land dom T \in dom z \land U (dom T) = z (dom T))) \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}$
52	26 30 39 41 49 50 51	syl213anc	$⊢ (((\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) = 2_{𝑜}) \land ((z \in B \land \neg U <_{s} z) \land z (dom T) = 2_{𝑜})) \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}$
53	52	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) = 2_{𝑜}) \land (z \in B \land \neg U <_{s} z)) \to (z (dom T) = 2_{𝑜} \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T})$
54	53	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) = 2_{𝑜}) \land z \in B) \to (\neg U <_{s} z \to (z (dom T) = 2_{𝑜} \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
55	54	a2d	$⊢ (((\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) = 2_{𝑜}) \land z \in B) \to ((\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \to (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
56	55	ralimdva	$⊢ ((\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) = 2_{𝑜}) \to (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \to \forall z \in B (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
57	56	impcom	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land ((\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) = 2_{𝑜})) \to \forall z \in B (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T})$
58	57	anassrs	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to \forall z \in B (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T})$
59		dmeq	$⊢ p = U \to dom p = dom U$
60	59	eleq2d	$⊢ p = U \to (dom T \in dom p \leftrightarrow dom T \in dom U)$
61		breq1	$⊢ p = U \to (p <_{s} z \leftrightarrow U <_{s} z)$
62	61	notbid	$⊢ p = U \to (\neg p <_{s} z \leftrightarrow \neg U <_{s} z)$
63		reseq1	$⊢ p = U \to {p ↾}_{suc dom T} = {U ↾}_{suc dom T}$
64	63	eqeq1d	$⊢ p = U \to ({p ↾}_{suc dom T} = {z ↾}_{suc dom T} \leftrightarrow {U ↾}_{suc dom T} = {z ↾}_{suc dom T})$
65	62 64	imbi12d	$⊢ p = U \to ((\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T}) \leftrightarrow (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
66	65	ralbidv	$⊢ p = U \to (\forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T}) \leftrightarrow \forall z \in B (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
67	60 66	anbi12d	$⊢ p = U \to ((dom T \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T})) \leftrightarrow (dom T \in dom U \land \forall z \in B (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T})))$
68	67	rspcev	$⊢ (U \in B \land (dom T \in dom U \land \forall z \in B (\neg U <_{s} z \to {U ↾}_{suc dom T} = {z ↾}_{suc dom T}))) \to \exists p \in B (dom T \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
69	10 19 58 68	syl12anc	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to \exists p \in B (dom T \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
70		nodmon	$⊢ T \in No \to dom T \in On$
71	4 70	syl	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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 On$
72	71	adantr	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to dom T \in On$
73		eleq1	$⊢ a = dom T \to (a \in dom p \leftrightarrow dom T \in dom p)$
74		suceq	$⊢ a = dom T \to suc a = suc dom T$
75	74	reseq2d	$⊢ a = dom T \to {p ↾}_{suc a} = {p ↾}_{suc dom T}$
76	74	reseq2d	$⊢ a = dom T \to {z ↾}_{suc a} = {z ↾}_{suc dom T}$
77	75 76	eqeq12d	$⊢ a = dom T \to ({p ↾}_{suc a} = {z ↾}_{suc a} \leftrightarrow {p ↾}_{suc dom T} = {z ↾}_{suc dom T})$
78	77	imbi2d	$⊢ a = dom T \to ((\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}) \leftrightarrow (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
79	78	ralbidv	$⊢ a = dom T \to (\forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}) \leftrightarrow \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T}))$
80	73 79	anbi12d	$⊢ a = dom T \to ((a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a})) \leftrightarrow (dom T \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T})))$
81	80	rexbidv	$⊢ a = dom T \to (\exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a})) \leftrightarrow \exists p \in B (dom T \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T})))$
82	81	elabg	$⊢ dom T \in On \to (dom T \in \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\} \leftrightarrow \exists p \in B (dom T \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T})))$
83	72 82	syl	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to (dom T \in \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\} \leftrightarrow \exists p \in B (dom T \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc dom T} = {z ↾}_{suc dom T})))$
84	69 83	mpbird	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to dom T \in \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\}$
85	1	noinfdm	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to dom T = \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\}$
86	85	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 = \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\}$
87	86	adantl	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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 = \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\}$
88	87	adantr	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to dom T = \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\}$
89	88	eleq2d	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to (dom T \in dom T \leftrightarrow dom T \in \{a \| \exists p \in B (a \in dom p \land \forall z \in B (\neg p <_{s} z \to {p ↾}_{suc a} = {z ↾}_{suc a}))\})$
90	84 89	mpbird	$⊢ ((\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}) \to dom T \in dom T$
91	8 90	mtand	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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) = 2_{𝑜}$
92	91	neqned	$⊢ (\forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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 2_{𝑜}$
93		rexanali	$⊢ \exists z \in B (\neg U <_{s} z \land \neg z (dom T) = 2_{𝑜}) \leftrightarrow \neg \forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜})$
94		simpr1	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 \exists x \in B \forall y \in B \neg y <_{s} x$
95		simpr2	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 (B \subseteq No \land B \in V)$
96		simplll	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 z \in B$
97		simpr3	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 \in B \land {U ↾}_{dom T} = T)$
98		simpll	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 (z \in B \land \neg U <_{s} z)$
99	94 95 97 98 37	syl112anc	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 {z ↾}_{dom T} = T$
100	1	noinfbnd1lem4	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land (z \in B \land {z ↾}_{dom T} = T)) \to z (dom T) \neq \emptyset$
101	94 95 96 99 100	syl112anc	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 z (dom T) \neq \emptyset$
102	101	neneqd	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 z (dom T) = \emptyset$
103	102	pm2.21d	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 (z (dom T) = \emptyset \to U (dom T) \neq 2_{𝑜})$
104	1	noinfbnd1lem3	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land (z \in B \land {z ↾}_{dom T} = T)) \to z (dom T) \neq 1_{𝑜}$
105	94 95 96 99 104	syl112anc	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 z (dom T) \neq 1_{𝑜}$
106	105	neneqd	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 z (dom T) = 1_{𝑜}$
107	106	pm2.21d	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 (z (dom T) = 1_{𝑜} \to U (dom T) \neq 2_{𝑜})$
108		simplr	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 z (dom T) = 2_{𝑜}$
109		simpr2l	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 B \subseteq No$
110	109 96	sseldd	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 z \in No$
111		nofv	$⊢ z \in No \to (z (dom T) = \emptyset \lor z (dom T) = 1_{𝑜} \lor z (dom T) = 2_{𝑜})$
112	110 111	syl	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 (z (dom T) = \emptyset \lor z (dom T) = 1_{𝑜} \lor z (dom T) = 2_{𝑜})$
113		3orel3	$⊢ \neg z (dom T) = 2_{𝑜} \to ((z (dom T) = \emptyset \lor z (dom T) = 1_{𝑜} \lor z (dom T) = 2_{𝑜}) \to (z (dom T) = \emptyset \lor z (dom T) = 1_{𝑜}))$
114	108 112 113	sylc	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 (z (dom T) = \emptyset \lor z (dom T) = 1_{𝑜})$
115	103 107 114	mpjaod	$⊢ (((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \land (\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 2_{𝑜}$
116	115	ex	$⊢ ((z \in B \land \neg U <_{s} z) \land \neg z (dom T) = 2_{𝑜}) \to ((\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 2_{𝑜})$
117	116	anasss	$⊢ (z \in B \land (\neg U <_{s} z \land \neg z (dom T) = 2_{𝑜})) \to ((\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 2_{𝑜})$
118	117	rexlimiva	$⊢ \exists z \in B (\neg U <_{s} z \land \neg z (dom T) = 2_{𝑜}) \to ((\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 2_{𝑜})$
119	118	imp	$⊢ (\exists z \in B (\neg U <_{s} z \land \neg z (dom T) = 2_{𝑜}) \land (\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 2_{𝑜}$
120	93 119	sylanbr	$⊢ (\neg \forall z \in B (\neg U <_{s} z \to z (dom T) = 2_{𝑜}) \land (\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 2_{𝑜}$
121	92 120	pm2.61ian	$⊢ (\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 2_{𝑜}$

Metamath Proof Explorer

Theorem noinfbnd1lem5

Proof