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