noinffv

Description: The value of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Hypothesis	noinffv.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	noinffv	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to T (G) = U (G)$

Proof

Step	Hyp	Ref	Expression
1		noinffv.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		iffalse	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to 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)))) = (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)))$
3	1 2	eqtrid	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to T = (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)))$
4	3	fveq1d	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to T (G) = (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))) (G)$
5	4	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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to T (G) = (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))) (G)$
6		dmeq	$⊢ u = U \to dom u = dom U$
7	6	eleq2d	$⊢ u = U \to (G \in dom u \leftrightarrow G \in dom U)$
8		breq1	$⊢ u = U \to (u <_{s} v \leftrightarrow U <_{s} v)$
9	8	notbid	$⊢ u = U \to (\neg u <_{s} v \leftrightarrow \neg U <_{s} v)$
10		reseq1	$⊢ u = U \to {u ↾}_{suc G} = {U ↾}_{suc G}$
11	10	eqeq1d	$⊢ u = U \to ({u ↾}_{suc G} = {v ↾}_{suc G} \leftrightarrow {U ↾}_{suc G} = {v ↾}_{suc G})$
12	9 11	imbi12d	$⊢ u = U \to ((\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))$
13	12	ralbidv	$⊢ u = U \to (\forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))$
14	7 13	anbi12d	$⊢ u = U \to ((G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})) \leftrightarrow (G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})))$
15	14	rspcev	$⊢ (U \in B \land (G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
16	15	3impb	$⊢ (U \in B \land G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
17	16	3ad2ant3	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
18		simp32	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to G \in dom U$
19		eleq1	$⊢ y = G \to (y \in dom u \leftrightarrow G \in dom u)$
20		suceq	$⊢ y = G \to suc y = suc G$
21	20	reseq2d	$⊢ y = G \to {u ↾}_{suc y} = {u ↾}_{suc G}$
22	20	reseq2d	$⊢ y = G \to {v ↾}_{suc y} = {v ↾}_{suc G}$
23	21 22	eqeq12d	$⊢ y = G \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc G} = {v ↾}_{suc G})$
24	23	imbi2d	$⊢ y = G \to ((\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
25	24	ralbidv	$⊢ y = G \to (\forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
26	19 25	anbi12d	$⊢ y = G \to ((y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})))$
27	26	rexbidv	$⊢ y = G \to (\exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})))$
28	27	elabg	$⊢ G \in dom U \to (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}))\} \leftrightarrow \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})))$
29	18 28	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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to (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}))\} \leftrightarrow \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})))$
30	17 29	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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to 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}))\}$
31		eleq1	$⊢ g = G \to (g \in dom u \leftrightarrow G \in dom u)$
32		suceq	$⊢ g = G \to suc g = suc G$
33	32	reseq2d	$⊢ g = G \to {u ↾}_{suc g} = {u ↾}_{suc G}$
34	32	reseq2d	$⊢ g = G \to {v ↾}_{suc g} = {v ↾}_{suc G}$
35	33 34	eqeq12d	$⊢ g = G \to ({u ↾}_{suc g} = {v ↾}_{suc g} \leftrightarrow {u ↾}_{suc G} = {v ↾}_{suc G})$
36	35	imbi2d	$⊢ g = G \to ((\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
37	36	ralbidv	$⊢ g = G \to (\forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
38		fveqeq2	$⊢ g = G \to (u (g) = x \leftrightarrow u (G) = x)$
39	31 37 38	3anbi123d	$⊢ g = G \to ((g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x) \leftrightarrow (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x))$
40	39	rexbidv	$⊢ g = G \to (\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) \leftrightarrow \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))$
41	40	iotabidv	$⊢ g = G \to (ι 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)) = (ι 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))$
42		eqid	$⊢ (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))) = (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)))$
43		iotaex	$⊢ (ι 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)) \in V$
44	41 42 43	fvmpt	$⊢ 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}))\} \to (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))) (G) = (ι 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))$
45	30 44	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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to (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))) (G) = (ι 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))$
46		simp1	$⊢ (U \in B \land G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to U \in B$
47		simp2	$⊢ (U \in B \land G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to G \in dom U$
48		simp3	$⊢ (U \in B \land G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})$
49		eqidd	$⊢ (U \in B \land G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to U (G) = U (G)$
50		fveq1	$⊢ u = U \to u (G) = U (G)$
51	50	eqeq1d	$⊢ u = U \to (u (G) = U (G) \leftrightarrow U (G) = U (G))$
52	7 13 51	3anbi123d	$⊢ u = U \to ((G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G)) \leftrightarrow (G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}) \land U (G) = U (G)))$
53	52	rspcev	$⊢ (U \in B \land (G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}) \land U (G) = U (G))) \to \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) = U (G))$
54	46 47 48 49 53	syl13anc	$⊢ (U \in B \land G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \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) = U (G))$
55	54	3ad2ant3	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \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) = U (G))$
56		fvex	$⊢ U (G) \in V$
57		eqid	$⊢ u (G) = u (G)$
58		fvex	$⊢ u (G) \in V$
59		eqeq2	$⊢ x = u (G) \to (u (G) = x \leftrightarrow u (G) = u (G))$
60	59	3anbi3d	$⊢ x = u (G) \to ((G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = u (G)))$
61	58 60	spcev	$⊢ (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = u (G)) \to \exists x (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
62	57 61	mp3an3	$⊢ (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})) \to \exists x (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
63	62	reximi	$⊢ \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})) \to \exists u \in B \exists x (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
64		rexcom4	$⊢ \exists u \in B \exists x (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow \exists 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)$
65	63 64	sylib	$⊢ \exists u \in B (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})) \to \exists 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)$
66	16 65	syl	$⊢ (U \in B \land G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \exists 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)$
67	66	3ad2ant3	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists 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)$
68		simp2l	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to B \subseteq No$
69		noinfprefixmo	$⊢ B \subseteq No \to \exists^{*} 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)$
70	68 69	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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists^{*} 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)$
71		df-eu	$⊢ \exists! 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) \leftrightarrow (\exists 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) \land \exists^{*} 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))$
72	67 70 71	sylanbrc	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists! 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)$
73		eqeq2	$⊢ x = U (G) \to (u (G) = x \leftrightarrow u (G) = U (G))$
74	73	3anbi3d	$⊢ x = U (G) \to ((G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow (G \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G)))$
75	74	rexbidv	$⊢ x = U (G) \to (\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) \leftrightarrow \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) = U (G)))$
76	75	iota2	$⊢ (U (G) \in V \land \exists! 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)) \to (\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) = U (G)) \leftrightarrow (ι 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)) = U (G))$
77	56 72 76	sylancr	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to (\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) = U (G)) \leftrightarrow (ι 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)) = U (G))$
78	55 77	mpbid	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to (ι 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)) = U (G)$
79	5 45 78	3eqtrd	$⊢ (\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 G \in dom U \land \forall v \in B (\neg U <_{s} v \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to T (G) = U (G)$

Metamath Proof Explorer

Theorem noinffv

Proof