Metamath Proof Explorer

Theorem sdclem1

Description: Lemma for sdc . (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses sdc.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
sdc.2 ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) → ( 𝜓 ↔ 𝜒 ) )
sdc.3 ⊢ ( 𝑛 = 𝑀 → ( 𝜓 ↔ 𝜏 ) )
sdc.4 ⊢ ( 𝑛 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
sdc.5 ⊢ ( ( 𝑔 = ℎ ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝜓 ↔ 𝜎 ) )
sdc.6 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sdc.7 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
sdc.8 ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
sdc.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
sdc.10 ⊢ 𝐽 = { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) }
sdc.11 ⊢ 𝐹 = ( 𝑤 ∈ 𝑍 , 𝑥 ∈ 𝐽 ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
Assertion sdclem1 ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )

Proof

Step Hyp Ref Expression
1 sdc.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 sdc.2 ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) → ( 𝜓 ↔ 𝜒 ) )
3 sdc.3 ⊢ ( 𝑛 = 𝑀 → ( 𝜓 ↔ 𝜏 ) )
4 sdc.4 ⊢ ( 𝑛 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
5 sdc.5 ⊢ ( ( 𝑔 = ℎ ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝜓 ↔ 𝜎 ) )
6 sdc.6 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 sdc.7 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8 sdc.8 ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
9 sdc.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
10 sdc.10 ⊢ 𝐽 = { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) }
11 sdc.11 ⊢ 𝐹 = ( 𝑤 ∈ 𝑍 , 𝑥 ∈ 𝐽 ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
12 1 fvexi ⊢ 𝑍 ∈ V
13 simpl ⊢ ( ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) → 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 )
14 ovex ⊢ ( 𝑀 ... 𝑛 ) ∈ V
15 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑀 ... 𝑛 ) ∈ V ) → ( 𝑔 ∈ ( 𝐴 ↑m ( 𝑀 ... 𝑛 ) ) ↔ 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ) )
16 6 14 15 sylancl ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐴 ↑m ( 𝑀 ... 𝑛 ) ) ↔ 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ) )
17 13 16 imbitrrid ⊢ ( 𝜑 → ( ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) → 𝑔 ∈ ( 𝐴 ↑m ( 𝑀 ... 𝑛 ) ) ) )
18 17 abssdv ⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ⊆ ( 𝐴 ↑m ( 𝑀 ... 𝑛 ) ) )
19 ovex ⊢ ( 𝐴 ↑m ( 𝑀 ... 𝑛 ) ) ∈ V
20 ssexg ⊢ ( ( { 𝑔 ∣ ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ⊆ ( 𝐴 ↑m ( 𝑀 ... 𝑛 ) ) ∧ ( 𝐴 ↑m ( 𝑀 ... 𝑛 ) ) ∈ V ) → { 𝑔 ∣ ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ∈ V )
21 18 19 20 sylancl ⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ∈ V )
22 21 ralrimivw ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 { 𝑔 ∣ ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ∈ V )
23 abrexex2g ⊢ ( ( 𝑍 ∈ V ∧ ∀ 𝑛 ∈ 𝑍 { 𝑔 ∣ ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ∈ V ) → { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ∈ V )
24 12 22 23 sylancr ⊢ ( 𝜑 → { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ∈ V )
25 10 24 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ V )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝐽 ∈ V )
27 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝑀 ∈ ℤ )
28 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
30 29 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝑀 ∈ 𝑍 )
31 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝑔 : { 𝑀 } ⟶ 𝐴 )
32 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
33 27 32 syl ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
34 33 feq2d ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ↔ 𝑔 : { 𝑀 } ⟶ 𝐴 ) )
35 31 34 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 )
36 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝜏 )
37 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑀 ) )
38 37 feq2d ⊢ ( 𝑛 = 𝑀 → ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ↔ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ) )
39 38 3 anbi12d ⊢ ( 𝑛 = 𝑀 → ( ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ( 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ 𝜏 ) ) )
40 39 rspcev ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ( 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ 𝜏 ) ) → ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) )
41 30 35 36 40 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) )
42 10 eqabri ⊢ ( 𝑔 ∈ 𝐽 ↔ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) )
43 41 42 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝑔 ∈ 𝐽 )
44 1 peano2uzs ⊢ ( 𝑘 ∈ 𝑍 → ( 𝑘 + 1 ) ∈ 𝑍 )
45 44 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) → ( 𝑘 + 1 ) ∈ 𝑍 )
46 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) → ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 )
47 simpr3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) → 𝜎 )
48 vex ⊢ ℎ ∈ V
49 ovex ⊢ ( 𝑘 + 1 ) ∈ V
50 5 a1i ⊢ ( 𝜑 → ( ( 𝑔 = ℎ ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝜓 ↔ 𝜎 ) ) )
51 48 49 50 sbc2iedv ⊢ ( 𝜑 → ( [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 ↔ 𝜎 ) )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) → ( [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 ↔ 𝜎 ) )
53 47 52 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) → [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 )
54 nfv ⊢ Ⅎ 𝑛 ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴
55 nfcv ⊢ Ⅎ 𝑛 ℎ
56 nfsbc1v ⊢ Ⅎ 𝑛 [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓
57 55 56 nfsbcw ⊢ Ⅎ 𝑛 [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓
58 54 57 nfan ⊢ Ⅎ 𝑛 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 )
59 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... ( 𝑘 + 1 ) ) )
60 59 feq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ↔ ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ) )
61 sbceq1a ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝜓 ↔ [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 ) )
62 61 sbcbidv ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( [ ℎ / 𝑔 ] 𝜓 ↔ [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 ) )
63 60 62 anbi12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 ) ↔ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 ) ) )
64 58 63 rspce ⊢ ( ( ( 𝑘 + 1 ) ∈ 𝑍 ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] [ ( 𝑘 + 1 ) / 𝑛 ] 𝜓 ) ) → ∃ 𝑛 ∈ 𝑍 ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 ) )
65 45 46 53 64 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) → ∃ 𝑛 ∈ 𝑍 ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 ) )
66 10 eleq2i ⊢ ( ℎ ∈ 𝐽 ↔ ℎ ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } )
67 nfcv ⊢ Ⅎ 𝑔 𝑍
68 nfv ⊢ Ⅎ 𝑔 ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴
69 nfsbc1v ⊢ Ⅎ 𝑔 [ ℎ / 𝑔 ] 𝜓
70 68 69 nfan ⊢ Ⅎ 𝑔 ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 )
71 67 70 nfrexw ⊢ Ⅎ 𝑔 ∃ 𝑛 ∈ 𝑍 ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 )
72 feq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ↔ ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ) )
73 sbceq1a ⊢ ( 𝑔 = ℎ → ( 𝜓 ↔ [ ℎ / 𝑔 ] 𝜓 ) )
74 72 73 anbi12d ⊢ ( 𝑔 = ℎ → ( ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 ) ) )
75 74 rexbidv ⊢ ( 𝑔 = ℎ → ( ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑛 ∈ 𝑍 ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 ) ) )
76 71 48 75 elabf ⊢ ( ℎ ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ↔ ∃ 𝑛 ∈ 𝑍 ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 ) )
77 66 76 bitri ⊢ ( ℎ ∈ 𝐽 ↔ ∃ 𝑛 ∈ 𝑍 ( ℎ : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ℎ / 𝑔 ] 𝜓 ) )
78 65 77 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) → ℎ ∈ 𝐽 )
79 78 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) → ℎ ∈ 𝐽 ) )
80 79 abssdv ⊢ ( 𝜑 → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ⊆ 𝐽 )
81 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ 𝑥 ∈ 𝐽 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ⊆ 𝐽 )
82 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝐽 ∈ V )
83 elpw2g ⊢ ( 𝐽 ∈ V → ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ 𝒫 𝐽 ↔ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ⊆ 𝐽 ) )
84 82 83 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ 𝒫 𝐽 ↔ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ⊆ 𝐽 ) )
85 81 84 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ 𝑥 ∈ 𝐽 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ 𝒫 𝐽 )
86 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑘 ) )
87 86 feq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ↔ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ) )
88 87 4 anbi12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) ) )
89 88 cbvrexvw ⊢ ( ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) )
90 9 reximdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ 𝑘 ∈ 𝑍 ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
91 rexcom4 ⊢ ( ∃ 𝑘 ∈ 𝑍 ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) )
92 90 91 imbitrdi ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
93 89 92 biimtrid ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) → ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
94 93 ss2abdv ⊢ ( 𝜑 → { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ⊆ { 𝑔 ∣ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
95 10 94 eqsstrid ⊢ ( 𝜑 → 𝐽 ⊆ { 𝑔 ∣ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
96 95 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ { 𝑔 ∣ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
97 vex ⊢ 𝑥 ∈ V
98 eqeq1 ⊢ ( 𝑔 = 𝑥 → ( 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ↔ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) )
99 98 3anbi2d ⊢ ( 𝑔 = 𝑥 → ( ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
100 99 rexbidv ⊢ ( 𝑔 = 𝑥 → ( ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
101 100 exbidv ⊢ ( 𝑔 = 𝑥 → ( ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
102 97 101 elab ⊢ ( 𝑥 ∈ { 𝑔 ∣ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ↔ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) )
103 96 102 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) )
104 abn0 ⊢ ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ≠ ∅ ↔ ∃ ℎ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) )
105 103 104 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ≠ ∅ )
106 105 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ 𝑥 ∈ 𝐽 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ≠ ∅ )
107 eldifsn ⊢ ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ ( 𝒫 𝐽 ∖ { ∅ } ) ↔ ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ 𝒫 𝐽 ∧ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ≠ ∅ ) )
108 85 106 107 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ 𝑥 ∈ 𝐽 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ ( 𝒫 𝐽 ∖ { ∅ } ) )
109 108 adantrl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽 ) ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ ( 𝒫 𝐽 ∖ { ∅ } ) )
110 109 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ∀ 𝑤 ∈ 𝑍 ∀ 𝑥 ∈ 𝐽 { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ ( 𝒫 𝐽 ∖ { ∅ } ) )
111 11 fmpo ⊢ ( ∀ 𝑤 ∈ 𝑍 ∀ 𝑥 ∈ 𝐽 { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ ( 𝒫 𝐽 ∖ { ∅ } ) ↔ 𝐹 : ( 𝑍 × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) )
112 110 111 sylib ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝐹 : ( 𝑍 × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) )
113 7 iftrued ⊢ ( 𝜑 → if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) = 𝑀 )
114 113 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = ( ℤ≥ ‘ 𝑀 ) )
115 114 1 eqtr4di ⊢ ( 𝜑 → ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑍 )
116 115 xpeq1d ⊢ ( 𝜑 → ( ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) × 𝐽 ) = ( 𝑍 × 𝐽 ) )
117 116 feq2d ⊢ ( 𝜑 → ( 𝐹 : ( ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) ↔ 𝐹 : ( 𝑍 × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) ) )
118 117 biimpar ⊢ ( ( 𝜑 ∧ 𝐹 : ( 𝑍 × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) ) → 𝐹 : ( ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) )
119 112 118 syldan ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → 𝐹 : ( ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) )
120 0z ⊢ 0 ∈ ℤ
121 120 elimel ⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ∈ ℤ
122 eqid ⊢ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
123 121 122 axdc4uz ⊢ ( ( 𝐽 ∈ V ∧ 𝑔 ∈ 𝐽 ∧ 𝐹 : ( ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) × 𝐽 ) ⟶ ( 𝒫 𝐽 ∖ { ∅ } ) ) → ∃ 𝑗 ( 𝑗 : ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟶ 𝐽 ∧ ( 𝑗 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑔 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) )
124 26 43 119 123 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ∃ 𝑗 ( 𝑗 : ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟶ 𝐽 ∧ ( 𝑗 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑔 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) )
125 27 iftrued ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) = 𝑀 )
126 125 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = ( ℤ≥ ‘ 𝑀 ) )
127 126 1 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑍 )
128 127 feq2d ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( 𝑗 : ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟶ 𝐽 ↔ 𝑗 : 𝑍 ⟶ 𝐽 ) )
129 89 abbii ⊢ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } = { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) }
130 10 129 eqtri ⊢ 𝐽 = { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) }
131 feq3 ⊢ ( 𝐽 = { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } → ( 𝑗 : 𝑍 ⟶ 𝐽 ↔ 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ) )
132 130 131 ax-mp ⊢ ( 𝑗 : 𝑍 ⟶ 𝐽 ↔ 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } )
133 128 132 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( 𝑗 : ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟶ 𝐽 ↔ 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ) )
134 125 fveqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ( 𝑗 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑔 ↔ ( 𝑗 ‘ 𝑀 ) = 𝑔 ) )
135 127 raleqdv ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) )
136 133 134 135 3anbi123d ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ( 𝑗 : ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟶ 𝐽 ∧ ( 𝑗 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑔 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ↔ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) )
137 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → 𝐴 ∈ 𝑉 )
138 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → 𝑀 ∈ ℤ )
139 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → ∃ 𝑔 ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
140 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → 𝜑 )
141 140 9 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
142 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
143 nfcv ⊢ Ⅎ 𝑘 𝑗
144 nfcv ⊢ Ⅎ 𝑘 𝑍
145 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 )
146 145 nfab ⊢ Ⅎ 𝑘 { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) }
147 143 144 146 nff ⊢ Ⅎ 𝑘 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) }
148 nfv ⊢ Ⅎ 𝑘 ( 𝑗 ‘ 𝑀 ) = 𝑔
149 nfcv ⊢ Ⅎ 𝑘 𝑚
150 130 146 nfcxfr ⊢ Ⅎ 𝑘 𝐽
151 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 )
152 151 nfab ⊢ Ⅎ 𝑘 { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) }
153 144 150 152 nfmpo ⊢ Ⅎ 𝑘 ( 𝑤 ∈ 𝑍 , 𝑥 ∈ 𝐽 ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
154 11 153 nfcxfr ⊢ Ⅎ 𝑘 𝐹
155 nfcv ⊢ Ⅎ 𝑘 ( 𝑗 ‘ 𝑚 )
156 149 154 155 nfov ⊢ Ⅎ 𝑘 ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) )
157 156 nfel2 ⊢ Ⅎ 𝑘 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) )
158 144 157 nfralw ⊢ Ⅎ 𝑘 ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) )
159 147 148 158 nf3an ⊢ Ⅎ 𝑘 ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) )
160 142 159 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) )
161 simpr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } )
162 161 132 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → 𝑗 : 𝑍 ⟶ 𝐽 )
163 31 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → 𝑔 : { 𝑀 } ⟶ 𝐴 )
164 simpr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → ( 𝑗 ‘ 𝑀 ) = 𝑔 )
165 138 32 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
166 164 165 feq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → ( ( 𝑗 ‘ 𝑀 ) : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ↔ 𝑔 : { 𝑀 } ⟶ 𝐴 ) )
167 163 166 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → ( 𝑗 ‘ 𝑀 ) : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 )
168 simpr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) )
169 fvoveq1 ⊢ ( 𝑚 = 𝑤 → ( 𝑗 ‘ ( 𝑚 + 1 ) ) = ( 𝑗 ‘ ( 𝑤 + 1 ) ) )
170 id ⊢ ( 𝑚 = 𝑤 → 𝑚 = 𝑤 )
171 fveq2 ⊢ ( 𝑚 = 𝑤 → ( 𝑗 ‘ 𝑚 ) = ( 𝑗 ‘ 𝑤 ) )
172 170 171 oveq12d ⊢ ( 𝑚 = 𝑤 → ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) = ( 𝑤 𝐹 ( 𝑗 ‘ 𝑤 ) ) )
173 169 172 eleq12d ⊢ ( 𝑚 = 𝑤 → ( ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ↔ ( 𝑗 ‘ ( 𝑤 + 1 ) ) ∈ ( 𝑤 𝐹 ( 𝑗 ‘ 𝑤 ) ) ) )
174 173 rspccva ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ∧ 𝑤 ∈ 𝑍 ) → ( 𝑗 ‘ ( 𝑤 + 1 ) ) ∈ ( 𝑤 𝐹 ( 𝑗 ‘ 𝑤 ) ) )
175 168 174 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) ∧ 𝑤 ∈ 𝑍 ) → ( 𝑗 ‘ ( 𝑤 + 1 ) ) ∈ ( 𝑤 𝐹 ( 𝑗 ‘ 𝑤 ) ) )
176 1 2 3 4 5 137 138 139 141 10 11 160 162 167 175 sdclem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) ∧ ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )
177 176 ex ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ( 𝑗 : 𝑍 ⟶ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ∧ ( 𝑗 ‘ 𝑀 ) = 𝑔 ∧ ∀ 𝑚 ∈ 𝑍 ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) ) )
178 136 177 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ( 𝑗 : ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟶ 𝐽 ∧ ( 𝑗 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑔 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) ) )
179 178 exlimdv ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ( ∃ 𝑗 ( 𝑗 : ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟶ 𝐽 ∧ ( 𝑗 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = 𝑔 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ( 𝑗 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑗 ‘ 𝑚 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) ) )
180 124 179 mpd ⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) ) → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )
181 8 180 exlimddv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )