constrextdg2lem

	Ref	Expression
Hypotheses	constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
	constrextdg2.1	$⊢ E = ℂ_{fld} ↾_{𝑠} e$
	constrextdg2.2	$⊢ F = ℂ_{fld} ↾_{𝑠} f$
	constrextdg2.l	$⊢ \underset{˙}{<} = \{⟨f, e⟩ \| (E /_{FldExt} F \land E [. : .] F = 2)\}$
	constrextdg2.n	$⊢ φ \to N \in ω$
	constrextdg2lem.1	$⊢ φ \to R \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}$
	constrextdg2lem.2	$⊢ φ \to R (0) = ℚ$
	constrextdg2lem.3	$⊢ φ \to C (N) \subseteq lastS (R)$
Assertion	constrextdg2lem	$⊢ φ \to \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (suc N) \subseteq lastS (v))$

Proof

Step	Hyp	Ref	Expression
1		constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
2		constrextdg2.1	$⊢ E = ℂ_{fld} ↾_{𝑠} e$
3		constrextdg2.2	$⊢ F = ℂ_{fld} ↾_{𝑠} f$
4		constrextdg2.l	$⊢ \underset{˙}{<} = \{⟨f, e⟩ \| (E /_{FldExt} F \land E [. : .] F = 2)\}$
5		constrextdg2.n	$⊢ φ \to N \in ω$
6		constrextdg2lem.1	$⊢ φ \to R \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}$
7		constrextdg2lem.2	$⊢ φ \to R (0) = ℚ$
8		constrextdg2lem.3	$⊢ φ \to C (N) \subseteq lastS (R)$
9		uneq2	$⊢ i = \emptyset \to C (N) \cup i = C (N) \cup \emptyset$
10	9	sseq1d	$⊢ i = \emptyset \to (C (N) \cup i \subseteq lastS (v) \leftrightarrow C (N) \cup \emptyset \subseteq lastS (v))$
11	10	anbi2d	$⊢ i = \emptyset \to ((v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow (v (0) = ℚ \land C (N) \cup \emptyset \subseteq lastS (v)))$
12	11	rexbidv	$⊢ i = \emptyset \to (\exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup \emptyset \subseteq lastS (v)))$
13		uneq2	$⊢ i = g \to C (N) \cup i = C (N) \cup g$
14	13	sseq1d	$⊢ i = g \to (C (N) \cup i \subseteq lastS (v) \leftrightarrow C (N) \cup g \subseteq lastS (v))$
15	14	anbi2d	$⊢ i = g \to ((v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow (v (0) = ℚ \land C (N) \cup g \subseteq lastS (v)))$
16	15	rexbidv	$⊢ i = g \to (\exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup g \subseteq lastS (v)))$
17		fveq1	$⊢ v = u \to v (0) = u (0)$
18	17	eqeq1d	$⊢ v = u \to (v (0) = ℚ \leftrightarrow u (0) = ℚ)$
19		fveq2	$⊢ v = u \to lastS (v) = lastS (u)$
20	19	sseq2d	$⊢ v = u \to (C (N) \cup i \subseteq lastS (v) \leftrightarrow C (N) \cup i \subseteq lastS (u))$
21	18 20	anbi12d	$⊢ v = u \to ((v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow (u (0) = ℚ \land C (N) \cup i \subseteq lastS (u)))$
22	21	cbvrexvw	$⊢ \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup i \subseteq lastS (u))$
23		uneq2	$⊢ i = g \cup \{y\} \to C (N) \cup i = C (N) \cup (g \cup \{y\})$
24	23	sseq1d	$⊢ i = g \cup \{y\} \to (C (N) \cup i \subseteq lastS (u) \leftrightarrow C (N) \cup (g \cup \{y\}) \subseteq lastS (u))$
25	24	anbi2d	$⊢ i = g \cup \{y\} \to ((u (0) = ℚ \land C (N) \cup i \subseteq lastS (u)) \leftrightarrow (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u)))$
26	25	rexbidv	$⊢ i = g \cup \{y\} \to (\exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup i \subseteq lastS (u)) \leftrightarrow \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u)))$
27	22 26	bitrid	$⊢ i = g \cup \{y\} \to (\exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u)))$
28		uneq2	$⊢ i = C (suc N) \to C (N) \cup i = C (N) \cup C (suc N)$
29	28	sseq1d	$⊢ i = C (suc N) \to (C (N) \cup i \subseteq lastS (v) \leftrightarrow C (N) \cup C (suc N) \subseteq lastS (v))$
30	29	anbi2d	$⊢ i = C (suc N) \to ((v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow (v (0) = ℚ \land C (N) \cup C (suc N) \subseteq lastS (v)))$
31	30	rexbidv	$⊢ i = C (suc N) \to (\exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup i \subseteq lastS (v)) \leftrightarrow \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup C (suc N) \subseteq lastS (v)))$
32		fveq1	$⊢ v = R \to v (0) = R (0)$
33	32	eqeq1d	$⊢ v = R \to (v (0) = ℚ \leftrightarrow R (0) = ℚ)$
34		fveq2	$⊢ v = R \to lastS (v) = lastS (R)$
35	34	sseq2d	$⊢ v = R \to (C (N) \cup \emptyset \subseteq lastS (v) \leftrightarrow C (N) \cup \emptyset \subseteq lastS (R))$
36	33 35	anbi12d	$⊢ v = R \to ((v (0) = ℚ \land C (N) \cup \emptyset \subseteq lastS (v)) \leftrightarrow (R (0) = ℚ \land C (N) \cup \emptyset \subseteq lastS (R)))$
37		un0	$⊢ C (N) \cup \emptyset = C (N)$
38	37 8	eqsstrid	$⊢ φ \to C (N) \cup \emptyset \subseteq lastS (R)$
39	7 38	jca	$⊢ φ \to (R (0) = ℚ \land C (N) \cup \emptyset \subseteq lastS (R))$
40	36 6 39	rspcedvdw	$⊢ φ \to \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup \emptyset \subseteq lastS (v))$
41		fveq1	$⊢ u = v \to u (0) = v (0)$
42	41	eqeq1d	$⊢ u = v \to (u (0) = ℚ \leftrightarrow v (0) = ℚ)$
43		fveq2	$⊢ u = v \to lastS (u) = lastS (v)$
44	43	sseq2d	$⊢ u = v \to (C (N) \cup (g \cup \{y\}) \subseteq lastS (u) \leftrightarrow C (N) \cup (g \cup \{y\}) \subseteq lastS (v))$
45	42 44	anbi12d	$⊢ u = v \to ((u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u)) \leftrightarrow (v (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (v)))$
46		simpllr	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}$
47	46	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}$
48		simpllr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to v (0) = ℚ$
49		simpr	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to C (N) \cup g \subseteq lastS (v)$
50	49	unssad	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to C (N) \subseteq lastS (v)$
51	50	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to C (N) \subseteq lastS (v)$
52		simplr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to C (N) \cup g \subseteq lastS (v)$
53	52	unssbd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to g \subseteq lastS (v)$
54		simpr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to y \in lastS (v)$
55	54	snssd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to \{y\} \subseteq lastS (v)$
56	53 55	unssd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to g \cup \{y\} \subseteq lastS (v)$
57	51 56	unssd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to C (N) \cup (g \cup \{y\}) \subseteq lastS (v)$
58	48 57	jca	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to (v (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (v))$
59	45 47 58	rspcedvdw	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land y \in lastS (v)) \to \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u))$
60		fveq1	$⊢ u = v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \to u (0) = (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) (0)$
61	60	eqeq1d	$⊢ u = v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \to (u (0) = ℚ \leftrightarrow (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) (0) = ℚ)$
62		fveq2	$⊢ u = v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \to lastS (u) = lastS (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩)$
63	62	sseq2d	$⊢ u = v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \to (C (N) \cup (g \cup \{y\}) \subseteq lastS (u) \leftrightarrow C (N) \cup (g \cup \{y\}) \subseteq lastS (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩))$
64	61 63	anbi12d	$⊢ u = v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \to ((u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u)) \leftrightarrow ((v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩)))$
65		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
66		cndrng	$⊢ ℂ_{fld} \in DivRing$
67	66	a1i	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to ℂ_{fld} \in DivRing$
68	46	chnwrd	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to v \in Word SubDRing (ℂ_{fld})$
69		simpr	$⊢ ((φ \land C (N) \cup g \subseteq lastS (v)) \land v = \emptyset) \to v = \emptyset$
70	69	fveq2d	$⊢ ((φ \land C (N) \cup g \subseteq lastS (v)) \land v = \emptyset) \to lastS (v) = lastS (\emptyset)$
71		lsw0g	$⊢ lastS (\emptyset) = \emptyset$
72	70 71	eqtrdi	$⊢ ((φ \land C (N) \cup g \subseteq lastS (v)) \land v = \emptyset) \to lastS (v) = \emptyset$
73		simplr	$⊢ ((φ \land C (N) \cup g \subseteq lastS (v)) \land v = \emptyset) \to C (N) \cup g \subseteq lastS (v)$
74		ssun1	$⊢ C (N) \subseteq C (N) \cup g$
75		nnon	$⊢ N \in ω \to N \in On$
76	5 75	syl	$⊢ φ \to N \in On$
77	1 76	constr01	$⊢ φ \to \{0, 1\} \subseteq C (N)$
78		c0ex	$⊢ 0 \in V$
79	78	prnz	$⊢ \{0, 1\} \neq \emptyset$
80		ssn0	$⊢ (\{0, 1\} \subseteq C (N) \land \{0, 1\} \neq \emptyset) \to C (N) \neq \emptyset$
81	77 79 80	sylancl	$⊢ φ \to C (N) \neq \emptyset$
82		ssn0	$⊢ (C (N) \subseteq C (N) \cup g \land C (N) \neq \emptyset) \to C (N) \cup g \neq \emptyset$
83	74 81 82	sylancr	$⊢ φ \to C (N) \cup g \neq \emptyset$
84	83	ad2antrr	$⊢ ((φ \land C (N) \cup g \subseteq lastS (v)) \land v = \emptyset) \to C (N) \cup g \neq \emptyset$
85		ssn0	$⊢ (C (N) \cup g \subseteq lastS (v) \land C (N) \cup g \neq \emptyset) \to lastS (v) \neq \emptyset$
86	73 84 85	syl2anc	$⊢ ((φ \land C (N) \cup g \subseteq lastS (v)) \land v = \emptyset) \to lastS (v) \neq \emptyset$
87	86	neneqd	$⊢ ((φ \land C (N) \cup g \subseteq lastS (v)) \land v = \emptyset) \to \neg lastS (v) = \emptyset$
88	72 87	pm2.65da	$⊢ (φ \land C (N) \cup g \subseteq lastS (v)) \to \neg v = \emptyset$
89	88	neqned	$⊢ (φ \land C (N) \cup g \subseteq lastS (v)) \to v \neq \emptyset$
90	89	ad4antr	$⊢ (((((φ \land C (N) \cup g \subseteq lastS (v)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land g \subseteq C (suc N)) \to v \neq \emptyset$
91	90	an62ds	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to v \neq \emptyset$
92		lswcl	$⊢ (v \in Word SubDRing (ℂ_{fld}) \land v \neq \emptyset) \to lastS (v) \in SubDRing (ℂ_{fld})$
93	68 91 92	syl2anc	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to lastS (v) \in SubDRing (ℂ_{fld})$
94	93	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to lastS (v) \in SubDRing (ℂ_{fld})$
95	65	sdrgss	$⊢ lastS (v) \in SubDRing (ℂ_{fld}) \to lastS (v) \subseteq ℂ$
96	94 95	syl	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to lastS (v) \subseteq ℂ$
97		onsuc	$⊢ N \in On \to suc N \in On$
98	76 97	syl	$⊢ φ \to suc N \in On$
99	1 98	constrsscn	$⊢ φ \to C (suc N) \subseteq ℂ$
100	99	ad6antr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to C (suc N) \subseteq ℂ$
101		simp-4r	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to y \in (C (suc N) ∖ g)$
102	101	eldifad	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to y \in C (suc N)$
103	102	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to y \in C (suc N)$
104	100 103	sseldd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to y \in ℂ$
105	104	snssd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to \{y\} \subseteq ℂ$
106	96 105	unssd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to lastS (v) \cup \{y\} \subseteq ℂ$
107	65 67 106	fldgensdrg	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to ℂ_{fld} fldGen (lastS (v) \cup \{y\}) \in SubDRing (ℂ_{fld})$
108	46	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}$
109	94	elexd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to lastS (v) \in V$
110	107	elexd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to ℂ_{fld} fldGen (lastS (v) \cup \{y\}) \in V$
111		eqid	$⊢ ℂ_{fld} ↾_{𝑠} lastS (v) = ℂ_{fld} ↾_{𝑠} lastS (v)$
112		eqid	$⊢ ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))$
113		cnfldfld	$⊢ ℂ_{fld} \in Field$
114	113	a1i	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to ℂ_{fld} \in Field$
115	65 111 112 114 94 105	fldgenfldext	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} lastS (v))$
116		simpr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2$
117	2 3	breq12i	$⊢ E /_{FldExt} F \leftrightarrow (ℂ_{fld} ↾_{𝑠} e) /_{FldExt} (ℂ_{fld} ↾_{𝑠} f)$
118		oveq2	$⊢ e = ℂ_{fld} fldGen (lastS (v) \cup \{y\}) \to ℂ_{fld} ↾_{𝑠} e = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))$
119	118	adantl	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to ℂ_{fld} ↾_{𝑠} e = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))$
120		oveq2	$⊢ f = lastS (v) \to ℂ_{fld} ↾_{𝑠} f = ℂ_{fld} ↾_{𝑠} lastS (v)$
121	120	adantr	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to ℂ_{fld} ↾_{𝑠} f = ℂ_{fld} ↾_{𝑠} lastS (v)$
122	119 121	breq12d	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to ((ℂ_{fld} ↾_{𝑠} e) /_{FldExt} (ℂ_{fld} ↾_{𝑠} f) \leftrightarrow (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} lastS (v)))$
123	117 122	bitrid	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to (E /_{FldExt} F \leftrightarrow (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} lastS (v)))$
124	2 3	oveq12i	$⊢ E [. : .] F = (ℂ_{fld} ↾_{𝑠} e) [. : .] (ℂ_{fld} ↾_{𝑠} f)$
125	119 121	oveq12d	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to (ℂ_{fld} ↾_{𝑠} e) [. : .] (ℂ_{fld} ↾_{𝑠} f) = (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v))$
126	124 125	eqtrid	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to E [. : .] F = (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v))$
127	126	eqeq1d	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to (E [. : .] F = 2 \leftrightarrow (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2)$
128	123 127	anbi12d	$⊢ (f = lastS (v) \land e = ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \to ((E /_{FldExt} F \land E [. : .] F = 2) \leftrightarrow ((ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2))$
129	128 4	brabga	$⊢ (lastS (v) \in V \land ℂ_{fld} fldGen (lastS (v) \cup \{y\}) \in V) \to (lastS (v) \underset{˙}{<} (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) \leftrightarrow ((ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2))$
130	129	biimpar	$⊢ ((lastS (v) \in V \land ℂ_{fld} fldGen (lastS (v) \cup \{y\}) \in V) \land ((ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2)) \to lastS (v) \underset{˙}{<} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))$
131	109 110 115 116 130	syl22anc	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to lastS (v) \underset{˙}{<} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))$
132	131	olcd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to (v = \emptyset \lor lastS (v) \underset{˙}{<} (ℂ_{fld} fldGen (lastS (v) \cup \{y\})))$
133	107 108 132	chnccats1	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}$
134	68	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to v \in Word SubDRing (ℂ_{fld})$
135	107	s1cld	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \in Word SubDRing (ℂ_{fld})$
136		hashgt0	$⊢ (v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} \land v \neq \emptyset) \to 0 < \|v\|$
137	46 91 136	syl2anc	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to 0 < \|v\|$
138	137	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to 0 < \|v\|$
139		ccatfv0	$⊢ (v \in Word SubDRing (ℂ_{fld}) \land ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩ \in Word SubDRing (ℂ_{fld}) \land 0 < \|v\|) \to (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) (0) = v (0)$
140	134 135 138 139	syl3anc	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) (0) = v (0)$
141		simpllr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to v (0) = ℚ$
142	140 141	eqtrd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) (0) = ℚ$
143	50	adantr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to C (N) \subseteq lastS (v)$
144		ssun3	$⊢ C (N) \subseteq lastS (v) \to C (N) \subseteq lastS (v) \cup \{y\}$
145	143 144	syl	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to C (N) \subseteq lastS (v) \cup \{y\}$
146		simplr	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to C (N) \cup g \subseteq lastS (v)$
147	146	unssbd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to g \subseteq lastS (v)$
148		ssun3	$⊢ g \subseteq lastS (v) \to g \subseteq lastS (v) \cup \{y\}$
149	147 148	syl	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to g \subseteq lastS (v) \cup \{y\}$
150		ssun2	$⊢ \{y\} \subseteq lastS (v) \cup \{y\}$
151	150	a1i	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to \{y\} \subseteq lastS (v) \cup \{y\}$
152	149 151	unssd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to g \cup \{y\} \subseteq lastS (v) \cup \{y\}$
153	145 152	unssd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to C (N) \cup (g \cup \{y\}) \subseteq lastS (v) \cup \{y\}$
154	65 67 106	fldgenssid	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to lastS (v) \cup \{y\} \subseteq ℂ_{fld} fldGen (lastS (v) \cup \{y\})$
155	153 154	sstrd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to C (N) \cup (g \cup \{y\}) \subseteq ℂ_{fld} fldGen (lastS (v) \cup \{y\})$
156		lswccats1	$⊢ (v \in Word SubDRing (ℂ_{fld}) \land ℂ_{fld} fldGen (lastS (v) \cup \{y\}) \in SubDRing (ℂ_{fld})) \to lastS (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) = ℂ_{fld} fldGen (lastS (v) \cup \{y\})$
157	134 107 156	syl2anc	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to lastS (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) = ℂ_{fld} fldGen (lastS (v) \cup \{y\})$
158	155 157	sseqtrrd	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to C (N) \cup (g \cup \{y\}) \subseteq lastS (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩)$
159	142 158	jca	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to ((v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩) (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (v ++ ⟨“ (ℂ_{fld} fldGen (lastS (v) \cup \{y\})) ”⟩))$
160	64 133 159	rspcedvdw	$⊢ ((((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2) \to \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u))$
161	76	ad5antr	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to N \in On$
162	1 111 112 93 161 50 102	constrelextdg2	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to (y \in lastS (v) \lor (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (lastS (v) \cup \{y\}))) [. : .] (ℂ_{fld} ↾_{𝑠} lastS (v)) = 2)$
163	59 160 162	mpjaodan	$⊢ (((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land v (0) = ℚ) \land C (N) \cup g \subseteq lastS (v)) \to \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u))$
164	163	anasss	$⊢ ((((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (N) \cup g \subseteq lastS (v))) \to \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u))$
165	164	rexlimdva2	$⊢ ((φ \land g \subseteq C (suc N)) \land y \in (C (suc N) ∖ g)) \to (\exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup g \subseteq lastS (v)) \to \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u)))$
166	165	anasss	$⊢ (φ \land (g \subseteq C (suc N) \land y \in (C (suc N) ∖ g))) \to (\exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup g \subseteq lastS (v)) \to \exists u \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (u (0) = ℚ \land C (N) \cup (g \cup \{y\}) \subseteq lastS (u)))$
167		peano2	$⊢ N \in ω \to suc N \in ω$
168	5 167	syl	$⊢ φ \to suc N \in ω$
169	1 168	constrfin	$⊢ φ \to C (suc N) \in Fin$
170	12 16 27 31 40 166 169	findcard2d	$⊢ φ \to \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup C (suc N) \subseteq lastS (v))$
171		simpr	$⊢ ((φ \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land C (N) \cup C (suc N) \subseteq lastS (v)) \to C (N) \cup C (suc N) \subseteq lastS (v)$
172	171	unssbd	$⊢ ((φ \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land C (N) \cup C (suc N) \subseteq lastS (v)) \to C (suc N) \subseteq lastS (v)$
173	172	ex	$⊢ (φ \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \to (C (N) \cup C (suc N) \subseteq lastS (v) \to C (suc N) \subseteq lastS (v))$
174	173	anim2d	$⊢ (φ \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \to ((v (0) = ℚ \land C (N) \cup C (suc N) \subseteq lastS (v)) \to (v (0) = ℚ \land C (suc N) \subseteq lastS (v)))$
175	174	reximdva	$⊢ φ \to (\exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (N) \cup C (suc N) \subseteq lastS (v)) \to \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (suc N) \subseteq lastS (v)))$
176	170 175	mpd	$⊢ φ \to \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (suc N) \subseteq lastS (v))$

Metamath Proof Explorer

Theorem constrextdg2lem

Proof