Metamath Proof Explorer

Theorem psrplusg

Description: The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses psrplusg.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrplusg.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrplusg.a ⊢ + = ( +g ‘ 𝑅 )
psrplusg.p ⊢ ✚ = ( +g ‘ 𝑆 )
Assertion psrplusg ✚ = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 psrplusg.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrplusg.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psrplusg.a ⊢ + = ( +g ‘ 𝑅 )
4 psrplusg.p ⊢ ✚ = ( +g ‘ 𝑆 )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 eqid ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
8 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
9 simpl ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐼 ∈ V )
10 1 5 8 2 9 psrbas ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
11 eqid ⊢ ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )
12 eqid ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
13 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) )
14 eqidd ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) = ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) )
15 simpr ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
16 1 5 3 6 7 8 10 11 12 13 14 9 15 psrval ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
17 16 fveq2d ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( +g ‘ 𝑆 ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
18 2 fvexi ⊢ 𝐵 ∈ V
19 18 18 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
20 ofexg ⊢ ( ( 𝐵 × 𝐵 ) ∈ V → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
21 psrvalstr ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) Struct ⟨ 1 , 9 ⟩
22 plusgid ⊢ +g = Slot ( +g ‘ ndx )
23 snsstp2 ⊢ { ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ }
24 ssun1 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
25 23 24 sstri ⊢ { ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
26 21 22 25 strfv ⊢ ( ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ∈ V → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
27 19 20 26 mp2b ⊢ ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
28 17 4 27 3eqtr4g ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ✚ = ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) )
29 reldmpsr ⊢ Rel dom mPwSer
30 29 ovprc ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
31 1 30 syl5eq ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑆 = ∅ )
32 31 fveq2d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( +g ‘ 𝑆 ) = ( +g ‘ ∅ ) )
33 22 str0 ⊢ ∅ = ( +g ‘ ∅ )
34 32 4 33 3eqtr4g ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ✚ = ∅ )
35 31 fveq2d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ 𝑆 ) = ( Base ‘ ∅ ) )
36 base0 ⊢ ∅ = ( Base ‘ ∅ )
37 35 2 36 3eqtr4g ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
38 37 xpeq2d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐵 × 𝐵 ) = ( 𝐵 × ∅ ) )
39 xp0 ⊢ ( 𝐵 × ∅ ) = ∅
40 38 39 eqtrdi ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐵 × 𝐵 ) = ∅ )
41 40 reseq2d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( ∘f + ↾ ∅ ) )
42 res0 ⊢ ( ∘f + ↾ ∅ ) = ∅
43 41 42 eqtrdi ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ∅ )
44 34 43 eqtr4d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ✚ = ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) )
45 28 44 pm2.61i ⊢ ✚ = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )