Metamath Proof Explorer

Theorem constrextdg2lem

Description: Lemma for constrextdg2 (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrextdg2.1 ⊢ 𝐸 = ( ℂfld ↾s 𝑒 )
constrextdg2.2 ⊢ 𝐹 = ( ℂfld ↾s 𝑓 )
constrextdg2.l ⊢ < = { ⟨ 𝑓 , 𝑒 ⟩ ∣ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 2 ) }
constrextdg2.n ⊢ ( 𝜑 → 𝑁 ∈ ω )
constrextdg2lem.1 ⊢ ( 𝜑 → 𝑅 ∈ ( < Chain ( SubDRing ‘ ℂfld ) ) )
constrextdg2lem.2 ⊢ ( 𝜑 → ( 𝑅 ‘ 0 ) = ℚ )
constrextdg2lem.3 ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ⊆ ( lastS ‘ 𝑅 ) )
Assertion constrextdg2lem ( 𝜑 → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂfld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ suc 𝑁 ) ⊆ ( lastS ‘ 𝑣 ) ) )

Proof

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