Metamath Proof Explorer

Theorem extvfvcl

Description: Closure for the "variable extension" function evaluated for converting a given polynomial F by adding a variable with index A . (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses extvfvvcl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
extvfvvcl.3 ⊢ 0 = ( 0g ‘ 𝑅 )
extvfvvcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
extvfvvcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
extvfvvcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
extvfvvcl.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
extvfvvcl.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
extvfvvcl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
extvfvvcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
extvfvcl.n ⊢ 𝑁 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
Assertion extvfvcl ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ 𝑁 )

Proof

Step Hyp Ref Expression
1 extvfvvcl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 extvfvvcl.3 ⊢ 0 = ( 0g ‘ 𝑅 )
3 extvfvvcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 extvfvvcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 extvfvvcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 extvfvvcl.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
7 extvfvvcl.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
8 extvfvvcl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
9 extvfvvcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
10 extvfvcl.n ⊢ 𝑁 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
11 5 fvexi ⊢ 𝐵 ∈ V
12 11 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
13 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
14 1 13 rabex2 ⊢ 𝐷 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
16 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ∈ V )
17 2 fvexi ⊢ 0 ∈ V
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 0 ∈ V )
19 16 18 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ∈ V )
20 1 2 3 4 8 6 7 9 extvfv ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )
21 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
22 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑅 ∈ Ring )
23 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝐼 )
24 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐹 ∈ 𝑀 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
26 1 2 21 22 5 6 7 23 24 25 extvfvvcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 )
27 19 20 26 fmpt2d ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) : 𝐷 ⟶ 𝐵 )
28 12 15 27 elmapdd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ ( 𝐵 ↑m 𝐷 ) )
29 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
30 1 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
31 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
32 29 5 30 31 3 psrbas ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐵 ↑m 𝐷 ) )
33 28 32 eleqtrrd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
34 15 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ∈ V )
35 17 a1i ⊢ ( 𝜑 → 0 ∈ V )
36 19 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) : 𝐷 ⟶ V )
37 36 ffund ⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )
38 fveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ‘ 𝐴 ) = ( 𝑥 ‘ 𝐴 ) )
39 38 eqeq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ‘ 𝐴 ) = 0 ↔ ( 𝑥 ‘ 𝐴 ) = 0 ) )
40 39 cbvrabv ⊢ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } = { 𝑥 ∈ 𝐷 ∣ ( 𝑥 ‘ 𝐴 ) = 0 }
41 40 partfun2 ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) )
42 41 oveq1i ⊢ ( ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) supp 0 ) = ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) ) supp 0 )
43 40 15 rabexd ⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∈ V )
44 43 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∈ V )
45 15 difexd ⊢ ( 𝜑 → ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∈ V )
46 45 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) ∈ V )
47 44 46 35 suppun2 ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) ) supp 0 ) = ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∪ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ) )
48 42 47 eqtrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) supp 0 ) = ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∪ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ) )
49 eqid ⊢ ( 𝐽 mPoly 𝑅 ) = ( 𝐽 mPoly 𝑅 )
50 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
51 50 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
52 49 5 7 51 9 mplelf ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ⟶ 𝐵 )
53 breq1 ⊢ ( ℎ = ( 𝑥 ↾ 𝐽 ) → ( ℎ finSupp 0 ↔ ( 𝑥 ↾ 𝐽 ) finSupp 0 ) )
54 nn0ex ⊢ ℕ0 ∈ V
55 54 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ℕ0 ∈ V )
56 3 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝐴 } ) ∈ V )
57 6 56 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ V )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝐽 ∈ V )
59 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝐼 ∈ 𝑉 )
60 ssrab2 ⊢ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⊆ 𝐷
61 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 )
62 61 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
63 1 62 eqsstrid ⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
64 60 63 sstrid ⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
65 64 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) )
66 59 55 65 elmaprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
67 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝐴 } ) ⊆ 𝐼 )
68 6 67 eqsstrid ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝐽 ⊆ 𝐼 )
70 66 69 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( 𝑥 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
71 55 58 70 elmapdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( 𝑥 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
72 60 a1i ⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⊆ 𝐷 )
73 72 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝑥 ∈ 𝐷 )
74 30 psrbagfsupp ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 finSupp 0 )
75 73 74 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 𝑥 finSupp 0 )
76 c0ex ⊢ 0 ∈ V
77 76 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → 0 ∈ V )
78 75 77 fsuppres ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( 𝑥 ↾ 𝐽 ) finSupp 0 )
79 53 71 78 elrabd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( 𝑥 ↾ 𝐽 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } )
80 52 79 cofmpt ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) )
81 80 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) )
82 43 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ∈ V )
83 suppco ⊢ ( ( 𝐹 ∈ 𝑀 ∧ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ∈ V ) → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) = ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) )
84 9 82 83 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) = ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) )
85 71 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⟶ ( ℕ0 ↑m 𝐽 ) )
86 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) )
87 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) )
88 reseq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ↾ 𝐽 ) = ( 𝑢 ↾ 𝐽 ) )
89 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } )
90 89 resexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ 𝐽 ) ∈ V )
91 87 88 89 90 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( 𝑢 ↾ 𝐽 ) )
92 reseq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 ↾ 𝐽 ) = ( 𝑣 ↾ 𝐽 ) )
93 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } )
94 93 resexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑣 ↾ 𝐽 ) ∈ V )
95 87 92 93 94 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) = ( 𝑣 ↾ 𝐽 ) )
96 86 91 95 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ 𝐽 ) = ( 𝑣 ↾ 𝐽 ) )
97 6 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝐽 = ( 𝐼 ∖ { 𝐴 } ) )
98 97 reseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ 𝐽 ) = ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) )
99 97 reseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑣 ↾ 𝐽 ) = ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) )
100 96 98 99 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) = ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) )
101 fveq1 ⊢ ( 𝑦 = 𝑢 → ( 𝑦 ‘ 𝐴 ) = ( 𝑢 ‘ 𝐴 ) )
102 101 eqeq1d ⊢ ( 𝑦 = 𝑢 → ( ( 𝑦 ‘ 𝐴 ) = 0 ↔ ( 𝑢 ‘ 𝐴 ) = 0 ) )
103 102 89 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ‘ 𝐴 ) = 0 )
104 fveq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ‘ 𝐴 ) = ( 𝑣 ‘ 𝐴 ) )
105 104 eqeq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑦 ‘ 𝐴 ) = 0 ↔ ( 𝑣 ‘ 𝐴 ) = 0 ) )
106 105 93 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑣 ‘ 𝐴 ) = 0 )
107 103 106 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( 𝑢 ‘ 𝐴 ) = ( 𝑣 ‘ 𝐴 ) )
108 107 opeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ = ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ )
109 108 sneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } = { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } )
110 100 109 uneq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ( ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } ) = ( ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } ) )
111 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝐼 ∈ 𝑉 )
112 54 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → ℕ0 ∈ V )
113 63 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
114 60 89 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 ∈ 𝐷 )
115 113 114 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 ∈ ( ℕ0 ↑m 𝐼 ) )
116 111 112 115 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 : 𝐼 ⟶ ℕ0 )
117 116 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 Fn 𝐼 )
118 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝐴 ∈ 𝐼 )
119 fnsnsplit ⊢ ( ( 𝑢 Fn 𝐼 ∧ 𝐴 ∈ 𝐼 ) → 𝑢 = ( ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } ) )
120 117 118 119 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 = ( ( 𝑢 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑢 ‘ 𝐴 ) ⟩ } ) )
121 60 93 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 ∈ 𝐷 )
122 113 121 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 ∈ ( ℕ0 ↑m 𝐼 ) )
123 111 112 122 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 : 𝐼 ⟶ ℕ0 )
124 123 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 Fn 𝐼 )
125 fnsnsplit ⊢ ( ( 𝑣 Fn 𝐼 ∧ 𝐴 ∈ 𝐼 ) → 𝑣 = ( ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } ) )
126 124 118 125 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑣 = ( ( 𝑣 ↾ ( 𝐼 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , ( 𝑣 ‘ 𝐴 ) ⟩ } ) )
127 110 120 126 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) ) → 𝑢 = 𝑣 )
128 127 ex ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
129 128 anasss ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∧ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ) → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
130 129 ralrimivva ⊢ ( 𝜑 → ∀ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∀ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
131 dff13 ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) ↔ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⟶ ( ℕ0 ↑m 𝐽 ) ∧ ∀ 𝑢 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ∀ 𝑣 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
132 85 130 131 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) )
133 df-f1 ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) ↔ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ⟶ ( ℕ0 ↑m 𝐽 ) ∧ Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) )
134 133 simprbi ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) : { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } –1-1→ ( ℕ0 ↑m 𝐽 ) → Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) )
135 132 134 syl ⊢ ( 𝜑 → Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) )
136 49 7 2 9 mplelsfi ⊢ ( 𝜑 → 𝐹 finSupp 0 )
137 136 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
138 imafi ⊢ ( ( Fun ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ∧ ( 𝐹 supp 0 ) ∈ Fin ) → ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) ∈ Fin )
139 135 137 138 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) “ ( 𝐹 supp 0 ) ) ∈ Fin )
140 84 139 eqeltrd ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∈ Fin )
141 81 140 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∈ Fin )
142 fconstmpt ⊢ ( ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) × { 0 } ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 )
143 142 oveq1i ⊢ ( ( ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) × { 0 } ) supp 0 ) = ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 )
144 fczsupp0 ⊢ ( ( ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) × { 0 } ) supp 0 ) = ∅
145 143 144 eqtr3i ⊢ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) = ∅
146 0fi ⊢ ∅ ∈ Fin
147 145 146 eqeltri ⊢ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ∈ Fin
148 147 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ∈ Fin )
149 141 148 unfid ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ↦ ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) ) supp 0 ) ∪ ( ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∈ 𝐷 ∣ ( 𝑦 ‘ 𝐴 ) = 0 } ) ↦ 0 ) supp 0 ) ) ∈ Fin )
150 48 149 eqeltrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) supp 0 ) ∈ Fin )
151 34 35 37 150 isfsuppd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) finSupp 0 )
152 20 151 eqbrtrd ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) finSupp 0 )
153 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
154 153 29 31 2 10 mplelbas ⊢ ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ 𝑁 ↔ ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) finSupp 0 ) )
155 33 152 154 sylanbrc ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ∈ 𝑁 )