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	eqtrid	⊢ ( ¬ ( 𝐼 ∈ 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 + ↾ ( 𝐵 × 𝐵 ) )