This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem selvply1rhmlemb

Description: Lemma for selvply1rhm . (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses selvply1rhmlema.1 ⊢ 𝐵 = ( Base ‘ 𝑃 )
selvply1rhmlema.2 ⊢ 𝑃 = ( { 𝑋 } mPoly 𝑅 )
selvply1rhmlema.3 ⊢ · = ( .r ‘ 𝑃 )
selvply1rhmlema.4 ⊢ × = ( .r ‘ 𝑄 )
selvply1rhmlema.5 ⊢ 𝑄 = ( Poly1 ‘ 𝑅 )
selvply1rhmlema.6 ⊢ 𝑀 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
selvply1rhmlema.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
selvply1rhmlema.8 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
selvply1rhmlema.9 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
selvply1rhmlemb.10 ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion selvply1rhmlemb ( 𝜑 → ( 𝑀 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝑀 ‘ 𝐹 ) × ( 𝑀 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 selvply1rhmlema.1 ⊢ 𝐵 = ( Base ‘ 𝑃 )
2 selvply1rhmlema.2 ⊢ 𝑃 = ( { 𝑋 } mPoly 𝑅 )
3 selvply1rhmlema.3 ⊢ · = ( .r ‘ 𝑃 )
4 selvply1rhmlema.4 ⊢ × = ( .r ‘ 𝑄 )
5 selvply1rhmlema.5 ⊢ 𝑄 = ( Poly1 ‘ 𝑅 )
6 selvply1rhmlema.6 ⊢ 𝑀 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
7 selvply1rhmlema.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 selvply1rhmlema.8 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 selvply1rhmlema.9 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10 selvply1rhmlemb.10 ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
11 fveq1 ⊢ ( 𝑓 = ( 𝐹 · 𝐺 ) → ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( 𝐹 · 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
12 11 mpteq2dv ⊢ ( 𝑓 = ( 𝐹 · 𝐺 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐹 · 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
13 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
14 eqid ⊢ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } = { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 }
15 14 psrbasfsupp ⊢ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } = { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ ( ◡ 𝑔 “ ℕ ) ∈ Fin }
16 2 1 13 3 15 9 10 mplmul ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑚 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ 𝑚 } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑚 ∘f − 𝑗 ) ) ) ) ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 · 𝐺 ) = ( 𝑚 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ 𝑚 } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑚 ∘f − 𝑗 ) ) ) ) ) ) )
18 breq2 ⊢ ( 𝑚 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( 𝑙 ∘r ≤ 𝑚 ↔ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
19 18 rabbidv ⊢ ( 𝑚 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ 𝑚 } = { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } )
20 fvoveq1 ⊢ ( 𝑚 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( 𝐺 ‘ ( 𝑚 ∘f − 𝑗 ) ) = ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) )
21 20 oveq2d ⊢ ( 𝑚 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑚 ∘f − 𝑗 ) ) ) = ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) )
22 19 21 mpteq12dv ⊢ ( 𝑚 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ 𝑚 } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑚 ∘f − 𝑗 ) ) ) ) = ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) ) )
23 22 oveq2d ⊢ ( 𝑚 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( 𝑅 Σg ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ 𝑚 } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑚 ∘f − 𝑗 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) ) ) )
24 nfcv ⊢ Ⅎ 𝑗 ( ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) )
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
27 fveq2 ⊢ ( 𝑗 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) )
28 oveq2 ⊢ ( 𝑗 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) = ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) )
29 28 fveq2d ⊢ ( 𝑗 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } → ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) = ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) )
30 27 29 oveq12d ⊢ ( 𝑗 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } → ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) = ( ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) ) )
31 8 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑅 ∈ CMnd )
33 eqid ⊢ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } = { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } }
34 ovexd ⊢ ( 𝜑 → ( ℕ0 ↑m { 𝑋 } ) ∈ V )
35 14 34 rabexd ⊢ ( 𝜑 → { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∈ V )
36 33 35 rabexd ⊢ ( 𝜑 → { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ∈ V )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ∈ V )
38 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 0g ‘ 𝑅 ) ∈ V )
39 35 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∈ V )
40 ssrab2 ⊢ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ⊆ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 }
41 40 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ⊆ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } )
42 2 25 1 15 10 mplelf ⊢ ( 𝜑 → 𝐺 : { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝐺 : { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
44 breq1 ⊢ ( 𝑔 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( 𝑔 finSupp 0 ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 ) )
45 nn0ex ⊢ ℕ0 ∈ V
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ℕ0 ∈ V )
47 snex ⊢ { 𝑋 } ∈ V
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ V )
49 7 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑋 ∈ 𝑉 )
50 1oex ⊢ 1o ∈ V
51 50 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 1o ∈ V )
52 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 ∈ ( ℕ0 ↑m 1o ) )
53 51 46 52 elmaprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 : 1o ⟶ ℕ0 )
54 0lt1o ⊢ ∅ ∈ 1o
55 54 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ∅ ∈ 1o )
56 53 55 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑛 ‘ ∅ ) ∈ ℕ0 )
57 49 56 fsnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
58 46 48 57 elmapdd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
59 snfi ⊢ { 𝑋 } ∈ Fin
60 59 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑋 } ∈ Fin )
61 c0ex ⊢ 0 ∈ V
62 61 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 0 ∈ V )
63 57 60 62 fdmfifsupp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
64 44 58 63 elrabd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } )
66 47 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { 𝑋 } ∈ V )
67 45 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ℕ0 ∈ V )
68 ssrab2 ⊢ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ⊆ ( ℕ0 ↑m { 𝑋 } )
69 40 68 sstri ⊢ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ⊆ ( ℕ0 ↑m { 𝑋 } )
70 69 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ⊆ ( ℕ0 ↑m { 𝑋 } ) )
71 70 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) )
72 66 67 71 elmaprd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑗 : { 𝑋 } ⟶ ℕ0 )
73 breq1 ⊢ ( 𝑙 = 𝑗 → ( 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ↔ 𝑗 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
74 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } )
75 73 74 elrabrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑗 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } )
76 15 psrbagcon ⊢ ( ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∧ 𝑗 : { 𝑋 } ⟶ ℕ0 ∧ 𝑗 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → ( ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∧ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
77 65 72 75 76 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∧ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
78 77 simpld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } )
79 43 78 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
80 2 25 1 15 9 mplelf ⊢ ( 𝜑 → 𝐹 : { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝐹 : { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
82 2 1 26 9 mplelsfi ⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
84 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
85 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
86 25 13 26 84 85 ringlzd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
87 38 38 39 41 79 81 83 86 fisuppov1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
88 ssidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
89 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑅 ∈ Ring )
90 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝐹 : { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
91 41 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑗 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } )
92 90 91 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( 𝐹 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
93 25 13 89 92 79 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
94 breq1 ⊢ ( 𝑙 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } → ( 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ↔ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
95 breq1 ⊢ ( 𝑔 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } → ( 𝑔 finSupp 0 ↔ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } finSupp 0 ) )
96 45 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ℕ0 ∈ V )
97 47 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { 𝑋 } ∈ V )
98 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑋 ∈ 𝑉 )
99 50 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 1o ∈ V )
100 ssrab2 ⊢ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ⊆ ( ℕ0 ↑m 1o )
101 100 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ⊆ ( ℕ0 ↑m 1o ) )
102 101 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 ∈ ( ℕ0 ↑m 1o ) )
103 99 96 102 elmaprd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 : 1o ⟶ ℕ0 )
104 54 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ∅ ∈ 1o )
105 103 104 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑖 ‘ ∅ ) ∈ ℕ0 )
106 98 105 fsnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
107 96 97 106 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ∈ ( ℕ0 ↑m { 𝑋 } ) )
108 59 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { 𝑋 } ∈ Fin )
109 61 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 0 ∈ V )
110 106 108 109 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } finSupp 0 )
111 95 107 110 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } )
112 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑛 ∈ ( ℕ0 ↑m 1o ) )
113 breq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∘r ≤ 𝑛 ↔ 𝑖 ∘r ≤ 𝑛 ) )
114 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } )
115 113 114 elrabrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 ∘r ≤ 𝑛 )
116 elmapfn ⊢ ( 𝑖 ∈ ( ℕ0 ↑m 1o ) → 𝑖 Fn 1o )
117 116 adantl ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) → 𝑖 Fn 1o )
118 elmapfn ⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) → 𝑛 Fn 1o )
119 118 adantr ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 Fn 1o )
120 50 a1i ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) → 1o ∈ V )
121 inidm ⊢ ( 1o ∩ 1o ) = 1o
122 eqidd ⊢ ( ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) ∧ ∅ ∈ 1o ) → ( 𝑖 ‘ ∅ ) = ( 𝑖 ‘ ∅ ) )
123 eqidd ⊢ ( ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) ∧ ∅ ∈ 1o ) → ( 𝑛 ‘ ∅ ) = ( 𝑛 ‘ ∅ ) )
124 117 119 120 120 121 122 123 ofrval ⊢ ( ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∘r ≤ 𝑛 ∧ ∅ ∈ 1o ) → ( 𝑖 ‘ ∅ ) ≤ ( 𝑛 ‘ ∅ ) )
125 112 102 115 104 124 syl211anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑖 ‘ ∅ ) ≤ ( 𝑛 ‘ ∅ ) )
126 125 ralrimivw ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ∀ 𝑥 ∈ { 𝑋 } ( 𝑖 ‘ ∅ ) ≤ ( 𝑛 ‘ ∅ ) )
127 106 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
128 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
129 128 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
130 inidm ⊢ ( { 𝑋 } ∩ { 𝑋 } ) = { 𝑋 }
131 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → 𝑥 ∈ { 𝑋 } )
132 131 elsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → 𝑥 = 𝑋 )
133 132 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) )
134 fvsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑖 ‘ ∅ ) ∈ ℕ0 ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) )
135 98 105 134 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) )
136 135 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) )
137 133 136 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑥 ) = ( 𝑖 ‘ ∅ ) )
138 132 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑋 ) )
139 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑛 ‘ ∅ ) ∈ ℕ0 )
140 fvsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑛 ‘ ∅ ) ∈ ℕ0 ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑛 ‘ ∅ ) )
141 98 139 140 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑛 ‘ ∅ ) )
142 141 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑛 ‘ ∅ ) )
143 138 142 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑥 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑥 ) = ( 𝑛 ‘ ∅ ) )
144 127 129 97 97 130 137 143 ofrfval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ↔ ∀ 𝑥 ∈ { 𝑋 } ( 𝑖 ‘ ∅ ) ≤ ( 𝑛 ‘ ∅ ) ) )
145 126 144 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } )
146 94 111 145 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } )
147 breq1 ⊢ ( 𝑘 = { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } → ( 𝑘 ∘r ≤ 𝑛 ↔ { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ∘r ≤ 𝑛 ) )
148 50 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 1o ∈ V )
149 df1o2 ⊢ 1o = { ∅ }
150 149 eqcomi ⊢ { ∅ } = 1o
151 150 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ∅ } = 1o )
152 0ex ⊢ ∅ ∈ V
153 152 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ∅ ∈ V )
154 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
155 7 154 syl ⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
156 155 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑋 ∈ { 𝑋 } )
157 72 156 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( 𝑗 ‘ 𝑋 ) ∈ ℕ0 )
158 153 157 fsnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } : { ∅ } ⟶ ℕ0 )
159 151 158 feq2dd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } : 1o ⟶ ℕ0 )
160 67 148 159 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ∈ ( ℕ0 ↑m 1o ) )
161 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑛 ∈ ( ℕ0 ↑m 1o ) )
162 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑋 ∈ 𝑉 )
163 161 162 jca ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) )
164 elmapfn ⊢ ( 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) → 𝑗 Fn { 𝑋 } )
165 164 adantr ⊢ ( ( 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) ) → 𝑗 Fn { 𝑋 } )
166 simpr ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
167 elmapi ⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) → 𝑛 : 1o ⟶ ℕ0 )
168 54 a1i ⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) → ∅ ∈ 1o )
169 167 168 ffvelcdmd ⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) → ( 𝑛 ‘ ∅ ) ∈ ℕ0 )
170 169 adantr ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑛 ‘ ∅ ) ∈ ℕ0 )
171 166 170 fsnd ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
172 171 ffnd ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
173 172 adantl ⊢ ( ( 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
174 47 a1i ⊢ ( ( 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) ) → { 𝑋 } ∈ V )
175 eqidd ⊢ ( ( ( 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) ) ∧ 𝑋 ∈ { 𝑋 } ) → ( 𝑗 ‘ 𝑋 ) = ( 𝑗 ‘ 𝑋 ) )
176 166 170 140 syl2anc ⊢ ( ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑛 ‘ ∅ ) )
177 176 ad2antlr ⊢ ( ( ( 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) ) ∧ 𝑋 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑛 ‘ ∅ ) )
178 165 173 174 174 130 175 177 ofrval ⊢ ( ( ( 𝑗 ∈ ( ℕ0 ↑m { 𝑋 } ) ∧ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ∧ 𝑋 ∈ 𝑉 ) ) ∧ 𝑗 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∧ 𝑋 ∈ { 𝑋 } ) → ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ ∅ ) )
179 71 163 75 156 178 syl211anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ ∅ ) )
180 fveq2 ⊢ ( 𝑜 = ∅ → ( 𝑛 ‘ 𝑜 ) = ( 𝑛 ‘ ∅ ) )
181 180 breq2d ⊢ ( 𝑜 = ∅ → ( ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ 𝑜 ) ↔ ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ ∅ ) ) )
182 152 181 ralsn ⊢ ( ∀ 𝑜 ∈ { ∅ } ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ 𝑜 ) ↔ ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ ∅ ) )
183 179 182 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ∀ 𝑜 ∈ { ∅ } ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ 𝑜 ) )
184 149 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 1o = { ∅ } )
185 183 184 raleqtrrdv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ∀ 𝑜 ∈ 1o ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ 𝑜 ) )
186 159 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } Fn 1o )
187 118 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → 𝑛 Fn 1o )
188 elsni ⊢ ( 𝑜 ∈ { ∅ } → 𝑜 = ∅ )
189 188 149 eleq2s ⊢ ( 𝑜 ∈ 1o → 𝑜 = ∅ )
190 189 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑜 ∈ 1o ) → 𝑜 = ∅ )
191 190 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑜 ∈ 1o ) → ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ 𝑜 ) = ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ ∅ ) )
192 157 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑜 ∈ 1o ) → ( 𝑗 ‘ 𝑋 ) ∈ ℕ0 )
193 fvsng ⊢ ( ( ∅ ∈ V ∧ ( 𝑗 ‘ 𝑋 ) ∈ ℕ0 ) → ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ ∅ ) = ( 𝑗 ‘ 𝑋 ) )
194 152 192 193 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑜 ∈ 1o ) → ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ ∅ ) = ( 𝑗 ‘ 𝑋 ) )
195 191 194 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑜 ∈ 1o ) → ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ 𝑜 ) = ( 𝑗 ‘ 𝑋 ) )
196 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑜 ∈ 1o ) → ( 𝑛 ‘ 𝑜 ) = ( 𝑛 ‘ 𝑜 ) )
197 186 187 148 148 121 195 196 ofrfval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ∘r ≤ 𝑛 ↔ ∀ 𝑜 ∈ 1o ( 𝑗 ‘ 𝑋 ) ≤ ( 𝑛 ‘ 𝑜 ) ) )
198 185 197 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ∘r ≤ 𝑛 )
199 147 160 198 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } )
200 eqcom ⊢ ( ( 𝑗 ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) ↔ ( 𝑖 ‘ ∅ ) = ( 𝑗 ‘ 𝑋 ) )
201 200 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( 𝑗 ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) ↔ ( 𝑖 ‘ ∅ ) = ( 𝑗 ‘ 𝑋 ) ) )
202 135 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) )
203 202 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( 𝑗 ‘ 𝑋 ) = ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) ↔ ( 𝑗 ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) ) )
204 157 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑗 ‘ 𝑋 ) ∈ ℕ0 )
205 152 204 193 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ ∅ ) = ( 𝑗 ‘ 𝑋 ) )
206 205 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( 𝑖 ‘ ∅ ) = ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ↔ ( 𝑖 ‘ ∅ ) = ( 𝑗 ‘ 𝑋 ) ) )
207 201 203 206 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( 𝑗 ‘ 𝑋 ) = ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) ↔ ( 𝑖 ‘ ∅ ) = ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ) )
208 162 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑋 ∈ 𝑉 )
209 eqid ⊢ { 𝑋 } = { 𝑋 }
210 72 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑗 : { 𝑋 } ⟶ ℕ0 )
211 210 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑗 Fn { 𝑋 } )
212 127 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
213 208 209 211 212 fsneq ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑗 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ↔ ( 𝑗 ‘ 𝑋 ) = ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) ) )
214 152 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ∅ ∈ V )
215 103 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 : 1o ⟶ ℕ0 )
216 215 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 Fn 1o )
217 186 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } Fn 1o )
218 214 149 216 217 fsneq ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑖 = { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ↔ ( 𝑖 ‘ ∅ ) = ( { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ‘ ∅ ) ) )
219 207 213 218 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑗 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ↔ 𝑖 = { ⟨ ∅ , ( 𝑗 ‘ 𝑋 ) ⟩ } ) )
220 199 219 reu6dv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ) → ∃! 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } 𝑗 = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } )
221 24 25 26 30 32 37 87 88 93 146 220 gsummptfsf1o ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) ) ) ) )
222 100 a1i ⊢ ( 𝜑 → { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ⊆ ( ℕ0 ↑m 1o ) )
223 222 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 ∈ ( ℕ0 ↑m 1o ) )
224 fveq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ‘ ∅ ) = ( 𝑖 ‘ ∅ ) )
225 224 opeq2d ⊢ ( 𝑛 = 𝑖 → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ )
226 225 sneqd ⊢ ( 𝑛 = 𝑖 → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } )
227 226 fveq2d ⊢ ( 𝑛 = 𝑖 → ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) )
228 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
229 228 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
230 ovexd ⊢ ( 𝜑 → ( ℕ0 ↑m 1o ) ∈ V )
231 230 mptexd ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ V )
232 6 229 9 231 fvmptd3 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
233 232 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑀 ‘ 𝐹 ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
234 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) → 𝑖 ∈ ( ℕ0 ↑m 1o ) )
235 fvexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ∈ V )
236 227 233 234 235 fvmptd4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) )
237 223 236 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) )
238 237 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) = ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) )
239 fveq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
240 239 mpteq2dv ⊢ ( 𝑓 = 𝐺 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
241 230 mptexd ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ V )
242 6 240 10 241 fvmptd3 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐺 ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
243 fveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
244 243 opeq2d ⊢ ( 𝑛 = 𝑚 → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
245 244 sneqd ⊢ ( 𝑛 = 𝑚 → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } )
246 245 fveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) )
247 246 cbvmptv ⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) )
248 242 247 eqtrdi ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐺 ) = ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) )
249 248 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑀 ‘ 𝐺 ) = ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) )
250 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → 𝑚 = ( 𝑛 ∘f − 𝑖 ) )
251 250 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( 𝑚 ‘ ∅ ) = ( ( 𝑛 ∘f − 𝑖 ) ‘ ∅ ) )
252 54 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ∅ ∈ 1o )
253 118 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 Fn 1o )
254 253 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → 𝑛 Fn 1o )
255 102 116 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 Fn 1o )
256 255 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → 𝑖 Fn 1o )
257 50 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → 1o ∈ V )
258 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) ∧ ∅ ∈ 1o ) → ( 𝑛 ‘ ∅ ) = ( 𝑛 ‘ ∅ ) )
259 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) ∧ ∅ ∈ 1o ) → ( 𝑖 ‘ ∅ ) = ( 𝑖 ‘ ∅ ) )
260 254 256 257 257 121 258 259 ofval ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) ∧ ∅ ∈ 1o ) → ( ( 𝑛 ∘f − 𝑖 ) ‘ ∅ ) = ( ( 𝑛 ‘ ∅ ) − ( 𝑖 ‘ ∅ ) ) )
261 252 260 mpdan ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( ( 𝑛 ∘f − 𝑖 ) ‘ ∅ ) = ( ( 𝑛 ‘ ∅ ) − ( 𝑖 ‘ ∅ ) ) )
262 251 261 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( 𝑚 ‘ ∅ ) = ( ( 𝑛 ‘ ∅ ) − ( 𝑖 ‘ ∅ ) ) )
263 98 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → 𝑋 ∈ 𝑉 )
264 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( 𝑚 ‘ ∅ ) ∈ V )
265 fvsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑚 ‘ ∅ ) ∈ V ) → ( { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑚 ‘ ∅ ) )
266 263 264 265 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑚 ‘ ∅ ) )
267 263 154 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → 𝑋 ∈ { 𝑋 } )
268 129 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
269 127 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
270 47 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → { 𝑋 } ∈ V )
271 141 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) ∧ 𝑋 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑛 ‘ ∅ ) )
272 135 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) ∧ 𝑋 ∈ { 𝑋 } ) → ( { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( 𝑖 ‘ ∅ ) )
273 268 269 270 270 130 271 272 ofval ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) ∧ 𝑋 ∈ { 𝑋 } ) → ( ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ‘ 𝑋 ) = ( ( 𝑛 ‘ ∅ ) − ( 𝑖 ‘ ∅ ) ) )
274 267 273 mpdan ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ‘ 𝑋 ) = ( ( 𝑛 ‘ ∅ ) − ( 𝑖 ‘ ∅ ) ) )
275 262 266 274 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ‘ 𝑋 ) )
276 elsni ⊢ ( 𝑥 ∈ { ( 𝑛 ‘ ∅ ) } → 𝑥 = ( 𝑛 ‘ ∅ ) )
277 276 adantr ⊢ ( ( 𝑥 ∈ { ( 𝑛 ‘ ∅ ) } ∧ 𝑦 ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ) → 𝑥 = ( 𝑛 ‘ ∅ ) )
278 277 oveq1d ⊢ ( ( 𝑥 ∈ { ( 𝑛 ‘ ∅ ) } ∧ 𝑦 ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ) → ( 𝑥 − 𝑦 ) = ( ( 𝑛 ‘ ∅ ) − 𝑦 ) )
279 fznn0sub2 ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) → ( ( 𝑛 ‘ ∅ ) − 𝑦 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
280 279 adantl ⊢ ( ( 𝑥 ∈ { ( 𝑛 ‘ ∅ ) } ∧ 𝑦 ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ) → ( ( 𝑛 ‘ ∅ ) − 𝑦 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
281 278 280 eqeltrd ⊢ ( ( 𝑥 ∈ { ( 𝑛 ‘ ∅ ) } ∧ 𝑦 ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ) → ( 𝑥 − 𝑦 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
282 281 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ ( 𝑥 ∈ { ( 𝑛 ‘ ∅ ) } ∧ 𝑦 ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ) ) → ( 𝑥 − 𝑦 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
283 fvex ⊢ ( 𝑛 ‘ ∅ ) ∈ V
284 152 283 f1osn ⊢ { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } : { ∅ } –1-1-onto→ { ( 𝑛 ‘ ∅ ) }
285 f1of ⊢ ( { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } : { ∅ } –1-1-onto→ { ( 𝑛 ‘ ∅ ) } → { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } : { ∅ } ⟶ { ( 𝑛 ‘ ∅ ) } )
286 284 285 mp1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } : { ∅ } ⟶ { ( 𝑛 ‘ ∅ ) } )
287 fvsng ⊢ ( ( ∅ ∈ V ∧ ( 𝑛 ‘ ∅ ) ∈ ℕ0 ) → ( { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } ‘ ∅ ) = ( 𝑛 ‘ ∅ ) )
288 152 56 287 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } ‘ ∅ ) = ( 𝑛 ‘ ∅ ) )
289 288 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑛 ‘ ∅ ) = ( { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } ‘ ∅ ) )
290 152 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ∅ ∈ V )
291 150 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ∅ } = 1o )
292 55 56 fsnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } : { ∅ } ⟶ ℕ0 )
293 291 292 feq2dd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } : 1o ⟶ ℕ0 )
294 293 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } Fn 1o )
295 290 149 253 294 fsneq ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑛 = { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } ↔ ( 𝑛 ‘ ∅ ) = ( { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } ‘ ∅ ) ) )
296 289 295 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 = { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } )
297 149 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 1o = { ∅ } )
298 296 297 feq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑛 : 1o ⟶ { ( 𝑛 ‘ ∅ ) } ↔ { ⟨ ∅ , ( 𝑛 ‘ ∅ ) ⟩ } : { ∅ } ⟶ { ( 𝑛 ‘ ∅ ) } ) )
299 286 298 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → 𝑛 : 1o ⟶ { ( 𝑛 ‘ ∅ ) } )
300 299 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑛 : 1o ⟶ { ( 𝑛 ‘ ∅ ) } )
301 149 fneq2i ⊢ ( 𝑖 Fn 1o ↔ 𝑖 Fn { ∅ } )
302 255 301 sylib ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 Fn { ∅ } )
303 0zd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 0 ∈ ℤ )
304 139 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑛 ‘ ∅ ) ∈ ℤ )
305 105 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑖 ‘ ∅ ) ∈ ℤ )
306 105 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 0 ≤ ( 𝑖 ‘ ∅ ) )
307 303 304 305 306 125 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑖 ‘ ∅ ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
308 fveq2 ⊢ ( 𝑜 = ∅ → ( 𝑖 ‘ 𝑜 ) = ( 𝑖 ‘ ∅ ) )
309 308 eleq1d ⊢ ( 𝑜 = ∅ → ( ( 𝑖 ‘ 𝑜 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ↔ ( 𝑖 ‘ ∅ ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ) )
310 152 309 ralsn ⊢ ( ∀ 𝑜 ∈ { ∅ } ( 𝑖 ‘ 𝑜 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ↔ ( 𝑖 ‘ ∅ ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
311 307 310 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ∀ 𝑜 ∈ { ∅ } ( 𝑖 ‘ 𝑜 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
312 ffnfv ⊢ ( 𝑖 : { ∅ } ⟶ ( 0 ... ( 𝑛 ‘ ∅ ) ) ↔ ( 𝑖 Fn { ∅ } ∧ ∀ 𝑜 ∈ { ∅ } ( 𝑖 ‘ 𝑜 ) ∈ ( 0 ... ( 𝑛 ‘ ∅ ) ) ) )
313 302 311 312 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → 𝑖 : { ∅ } ⟶ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
314 149 99 eqeltrrid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → { ∅ } ∈ V )
315 149 ineq2i ⊢ ( 1o ∩ 1o ) = ( 1o ∩ { ∅ } )
316 315 121 eqtr3i ⊢ ( 1o ∩ { ∅ } ) = 1o
317 282 300 313 99 314 316 off ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑛 ∘f − 𝑖 ) : 1o ⟶ ( 0 ... ( 𝑛 ‘ ∅ ) ) )
318 fz0ssnn0 ⊢ ( 0 ... ( 𝑛 ‘ ∅ ) ) ⊆ ℕ0
319 318 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 0 ... ( 𝑛 ‘ ∅ ) ) ⊆ ℕ0 )
320 317 319 fssd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑛 ∘f − 𝑖 ) : 1o ⟶ ℕ0 )
321 320 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( 𝑛 ∘f − 𝑖 ) : 1o ⟶ ℕ0 )
322 321 252 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( ( 𝑛 ∘f − 𝑖 ) ‘ ∅ ) ∈ ℕ0 )
323 251 322 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( 𝑚 ‘ ∅ ) ∈ ℕ0 )
324 263 323 fsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ0 )
325 324 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } Fn { 𝑋 } )
326 268 269 270 270 130 offn ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) Fn { 𝑋 } )
327 263 209 325 326 fsneq ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } = ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ↔ ( { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ‘ 𝑋 ) = ( ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ‘ 𝑋 ) ) )
328 275 327 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } = ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) )
329 328 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) ∧ 𝑚 = ( 𝑛 ∘f − 𝑖 ) ) → ( 𝐺 ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) = ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) )
330 96 99 320 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝑛 ∘f − 𝑖 ) ∈ ( ℕ0 ↑m 1o ) )
331 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) ∈ V )
332 249 329 330 331 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) = ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) )
333 238 332 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ) → ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) = ( ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) ) )
334 333 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) = ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) ) ) )
335 334 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( 𝐹 ‘ { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − { ⟨ 𝑋 , ( 𝑖 ‘ ∅ ) ⟩ } ) ) ) ) ) )
336 221 335 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∘f − 𝑗 ) ) ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) ) )
337 23 336 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) ∧ 𝑚 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑙 ∈ { 𝑔 ∈ ( ℕ0 ↑m { 𝑋 } ) ∣ 𝑔 finSupp 0 } ∣ 𝑙 ∘r ≤ 𝑚 } ↦ ( ( 𝐹 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑚 ∘f − 𝑗 ) ) ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) ) )
338 ovexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) ) ∈ V )
339 17 337 64 338 fvmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐹 · 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) ) )
340 339 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐹 · 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) ) ) )
341 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
342 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
343 5 342 ply1bas ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
344 5 341 4 ply1mulr ⊢ × = ( .r ‘ ( 1o mPoly 𝑅 ) )
345 psr1baslem ⊢ ( ℕ0 ↑m 1o ) = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
346 1 2 3 4 5 6 7 8 9 selvply1rhmlema ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐹 ) ∈ ( Base ‘ 𝑄 ) )
347 1 2 3 4 5 6 7 8 10 selvply1rhmlema ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐺 ) ∈ ( Base ‘ 𝑄 ) )
348 341 343 13 344 345 346 347 mplmul ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐹 ) × ( 𝑀 ‘ 𝐺 ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑅 Σg ( 𝑖 ∈ { 𝑘 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑘 ∘r ≤ 𝑛 } ↦ ( ( ( 𝑀 ‘ 𝐹 ) ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( ( 𝑀 ‘ 𝐺 ) ‘ ( 𝑛 ∘f − 𝑖 ) ) ) ) ) ) )
349 340 348 eqtr4d ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐹 · 𝐺 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( ( 𝑀 ‘ 𝐹 ) × ( 𝑀 ‘ 𝐺 ) ) )
350 12 349 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝐹 · 𝐺 ) ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑓 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( ( 𝑀 ‘ 𝐹 ) × ( 𝑀 ‘ 𝐺 ) ) )
351 47 a1i ⊢ ( 𝜑 → { 𝑋 } ∈ V )
352 2 351 8 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
353 1 3 352 9 10 ringcld ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
354 ovexd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐹 ) × ( 𝑀 ‘ 𝐺 ) ) ∈ V )
355 6 350 353 354 fvmptd2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 · 𝐺 ) ) = ( ( 𝑀 ‘ 𝐹 ) × ( 𝑀 ‘ 𝐺 ) ) )