Theorem ofoaid2

Description: Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025)

	Ref	Expression
Assertion	ofoaid2	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ) → ( ( 𝐴 × { ∅ } ) ∘f +o 𝐹 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐴 ∈ 𝑉 )
2		onss	⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
3		sstr	⊢ ( ( ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ On ) → ran 𝐹 ⊆ On )
4	3	expcom	⊢ ( 𝐵 ⊆ On → ( ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ On ) )
5	2 4	syl	⊢ ( 𝐵 ∈ On → ( ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ On ) )
6	5	anim2d	⊢ ( 𝐵 ∈ On → ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ On ) ) )
7		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
8		df-f	⊢ ( 𝐹 : 𝐴 ⟶ On ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ On ) )
9	6 7 8	3imtr4g	⊢ ( 𝐵 ∈ On → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 ⟶ On ) )
10		elmapi	⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
11	9 10	impel	⊢ ( ( 𝐵 ∈ On ∧ 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐹 : 𝐴 ⟶ On )
12	11	adantll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐹 : 𝐴 ⟶ On )
13		peano1	⊢ ∅ ∈ ω
14		fnconstg	⊢ ( ∅ ∈ ω → ( 𝐴 × { ∅ } ) Fn 𝐴 )
15	13 14	mp1i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ) → ( 𝐴 × { ∅ } ) Fn 𝐴 )
16		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) → ( 𝐴 × { ∅ } ) Fn 𝐴 )
17		simp2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) → 𝐹 : 𝐴 ⟶ On )
18	17	ffnd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) → 𝐹 Fn 𝐴 )
19		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) → 𝐴 ∈ 𝑉 )
20		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
21	16 18 19 19 20	offn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) → ( ( 𝐴 × { ∅ } ) ∘f +o 𝐹 ) Fn 𝐴 )
22	16 18	jca	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) → ( ( 𝐴 × { ∅ } ) Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) )
23	22	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐴 × { ∅ } ) Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) )
24	19	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → 𝐴 ∈ 𝑉 )
25		simpr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
26		fnfvof	⊢ ( ( ( ( 𝐴 × { ∅ } ) Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( ( 𝐴 × { ∅ } ) ∘f +o 𝐹 ) ‘ 𝑎 ) = ( ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) +o ( 𝐹 ‘ 𝑎 ) ) )
27	23 24 25 26	syl12anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐴 × { ∅ } ) ∘f +o 𝐹 ) ‘ 𝑎 ) = ( ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) +o ( 𝐹 ‘ 𝑎 ) ) )
28		fvconst2g	⊢ ( ( ∅ ∈ ω ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) = ∅ )
29	13 25 28	sylancr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) = ∅ )
30	29	oveq1d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) +o ( 𝐹 ‘ 𝑎 ) ) = ( ∅ +o ( 𝐹 ‘ 𝑎 ) ) )
31	17	ffvelcdmda	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ On )
32		oa0r	⊢ ( ( 𝐹 ‘ 𝑎 ) ∈ On → ( ∅ +o ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
33	31 32	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ∅ +o ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
34	27 30 33	3eqtrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐴 × { ∅ } ) ∘f +o 𝐹 ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
35	21 18 34	eqfnfvd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ On ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) → ( ( 𝐴 × { ∅ } ) ∘f +o 𝐹 ) = 𝐹 )
36	1 12 15 35	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ) → ( ( 𝐴 × { ∅ } ) ∘f +o 𝐹 ) = 𝐹 )