Metamath Proof Explorer

Theorem smflimmpt

Description: The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). A can contain m as a free variable, in other words it can be thought as an indexed collection A ( m ) . B can be thought as a collection with two indices B ( m , x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimmpt.p ⊢ Ⅎ 𝑚 𝜑
smflimmpt.x ⊢ Ⅎ 𝑥 𝜑
smflimmpt.n ⊢ Ⅎ 𝑛 𝜑
smflimmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflimmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimmpt.a ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐴 ∈ 𝑉 )
smflimmpt.b ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
smflimmpt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimmpt.l ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smflimmpt.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ }
smflimmpt.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
Assertion smflimmpt ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smflimmpt.p ⊢ Ⅎ 𝑚 𝜑
2 smflimmpt.x ⊢ Ⅎ 𝑥 𝜑
3 smflimmpt.n ⊢ Ⅎ 𝑛 𝜑
4 smflimmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 smflimmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 smflimmpt.a ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐴 ∈ 𝑉 )
7 smflimmpt.b ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
8 smflimmpt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
9 smflimmpt.l ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
10 smflimmpt.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ }
11 smflimmpt.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
12 11 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
13 10 a1i ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ } )
14 nfv ⊢ Ⅎ 𝑚 𝑛 ∈ 𝑍
15 1 14 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
16 5 uztrn2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
17 16 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
18 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
19 6 mptexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
20 18 17 19 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
21 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
22 21 fvmpt2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
23 17 20 22 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
24 23 dmeqd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
25 nfv ⊢ Ⅎ 𝑥 𝑛 ∈ 𝑍
26 2 25 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
27 nfv ⊢ Ⅎ 𝑥 𝑚 ∈ ( ℤ≥ ‘ 𝑛 )
28 26 27 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) )
29 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝜑 )
30 17 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑚 ∈ 𝑍 )
31 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
32 29 30 31 7 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
33 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
34 28 32 33 fnmptd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
35 34 fndmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
36 24 35 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐴 = dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
37 15 36 iineq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
38 3 37 iuneq2df ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
39 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
40 39 19 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
41 40 eqcomd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
42 41 dmeqd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
43 18 17 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
44 15 43 iineq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
45 3 44 iuneq2df ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
46 38 45 eqtr4d ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
47 46 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ↔ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
48 47 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
49 48 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
50 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
51 50 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
53 52 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
54 nfv ⊢ Ⅎ 𝑛 ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝
55 3 54 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
56 nfv ⊢ Ⅎ 𝑛 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝
57 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
58 nfcv ⊢ Ⅎ 𝑚 𝑥
59 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴
60 58 59 nfel ⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴
61 15 60 nfan ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
62 5 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
63 62 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ ℤ )
64 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
65 5 fvexi ⊢ 𝑍 ∈ V
66 65 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑍 ∈ V )
67 5 uzssd3 ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
68 67 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
69 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ V )
70 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
71 70 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
72 18 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
73 17 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
74 72 73 71 7 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐵 ∈ 𝑊 )
75 33 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
76 71 74 75 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
77 61 63 64 66 66 68 68 69 76 climeldmeqmpt3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) )
78 77 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) )
79 57 78 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
80 79 exp31 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) )
81 55 56 80 rexlimd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
82 81 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
83 53 82 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
84 49 83 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
85 84 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) )
86 47 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
87 86 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
88 87 51 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
89 3 56 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
90 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
91 77 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) )
92 90 91 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
93 92 exp31 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ) )
94 89 54 93 rexlimd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) )
95 94 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) )
96 88 95 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) → ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
97 87 96 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) )
98 97 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ) )
99 85 98 impbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) )
100 2 99 rabbida3 ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
101 13 100 eqtrd ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
102 10 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ } )
103 102 biimpi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ } )
104 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
105 103 104 51 3syl ⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
106 105 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
107 nfcv ⊢ Ⅎ 𝑛 𝑥
108 nfiu1 ⊢ Ⅎ 𝑛 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴
109 54 108 nfrabw ⊢ Ⅎ 𝑛 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ }
110 10 109 nfcxfr ⊢ Ⅎ 𝑛 𝐷
111 107 110 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ 𝐷
112 3 111 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
113 nfv ⊢ Ⅎ 𝑛 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) )
114 1 14 60 nf3an ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
115 simp2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ 𝑍 )
116 115 62 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ ℤ )
117 65 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑍 ∈ V )
118 5 115 uzssd2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
119 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ V )
120 70 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
121 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
122 115 16 sylan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
123 121 122 120 7 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐵 ∈ 𝑊 )
124 120 123 75 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
125 114 116 64 117 117 118 118 119 124 climfveqmpt3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
126 125 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) ) )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) ) )
128 112 113 127 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
129 106 128 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
130 129 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) )
131 2 101 130 mpteq12da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) ) )
132 41 eqcomd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
133 132 fveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
134 1 133 mpteq2da ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
135 134 eqcomd ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) )
136 135 eleq1d ⊢ ( 𝜑 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
137 2 45 136 rabbida2 ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
138 133 eqcomd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) )
139 1 138 mpteq2da ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) )
140 139 fveq2d ⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
141 2 137 140 mpteq12df ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
142 12 131 141 3eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
143 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
144 nfcv ⊢ Ⅎ 𝑥 𝑍
145 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
146 144 145 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
147 1 9 21 fmptdf ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
148 eqid ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
149 eqid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
150 143 146 4 5 8 147 148 149 smflim2 ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
151 142 150 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )