Metamath Proof Explorer

Theorem ofoafo

Description: Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoafo ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) –onto→ ( 𝐶 ↑m 𝐴 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
2 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
3 2 eqcomi ⊢ 𝐴 = ( 𝐴 ∩ 𝐴 )
4 3 a1i ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 = ( 𝐴 ∩ 𝐴 ) )
5 1 1 4 3jca ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 = ( 𝐴 ∩ 𝐴 ) ) )
6 ofoaf ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 = ( 𝐴 ∩ 𝐴 ) ) ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ⟶ ( 𝐶 ↑m 𝐴 ) )
7 5 6 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ⟶ ( 𝐶 ↑m 𝐴 ) )
8 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ) → ℎ ∈ ( 𝐶 ↑m 𝐴 ) )
9 omelon ⊢ ω ∈ On
10 9 a1i ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → ω ∈ On )
11 simpl ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → 𝐵 ∈ On )
12 10 11 jca ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → ( ω ∈ On ∧ 𝐵 ∈ On ) )
13 peano1 ⊢ ∅ ∈ ω
14 oen0 ⊢ ( ( ( ω ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝐵 ) )
15 12 13 14 sylancl ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → ∅ ∈ ( ω ↑o 𝐵 ) )
16 simpr ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → 𝐶 = ( ω ↑o 𝐵 ) )
17 15 16 eleqtrrd ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → ∅ ∈ 𝐶 )
18 fconst6g ⊢ ( ∅ ∈ 𝐶 → ( 𝐴 × { ∅ } ) : 𝐴 ⟶ 𝐶 )
19 17 18 syl ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → ( 𝐴 × { ∅ } ) : 𝐴 ⟶ 𝐶 )
20 19 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( 𝐴 × { ∅ } ) : 𝐴 ⟶ 𝐶 )
21 oecl ⊢ ( ( ω ∈ On ∧ 𝐵 ∈ On ) → ( ω ↑o 𝐵 ) ∈ On )
22 9 11 21 sylancr ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → ( ω ↑o 𝐵 ) ∈ On )
23 16 22 eqeltrd ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) → 𝐶 ∈ On )
24 23 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → 𝐶 ∈ On )
25 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → 𝐴 ∈ 𝑉 )
26 24 25 elmapd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ↔ ( 𝐴 × { ∅ } ) : 𝐴 ⟶ 𝐶 ) )
27 20 26 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) )
28 27 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ) → ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) )
29 ovres ⊢ ( ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) → ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) ( 𝐴 × { ∅ } ) ) = ( ℎ ∘f +o ( 𝐴 × { ∅ } ) ) )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) ( 𝐴 × { ∅ } ) ) = ( ℎ ∘f +o ( 𝐴 × { ∅ } ) ) )
31 elmapi ⊢ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) → ℎ : 𝐴 ⟶ 𝐶 )
32 31 adantr ⊢ ( ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) → ℎ : 𝐴 ⟶ 𝐶 )
33 32 ffnd ⊢ ( ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) → ℎ Fn 𝐴 )
34 33 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ℎ Fn 𝐴 )
35 elmapi ⊢ ( ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) → ( 𝐴 × { ∅ } ) : 𝐴 ⟶ 𝐶 )
36 35 adantl ⊢ ( ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) → ( 𝐴 × { ∅ } ) : 𝐴 ⟶ 𝐶 )
37 36 ffnd ⊢ ( ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) → ( 𝐴 × { ∅ } ) Fn 𝐴 )
38 37 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( 𝐴 × { ∅ } ) Fn 𝐴 )
39 25 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → 𝐴 ∈ 𝑉 )
40 34 38 39 39 2 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( ℎ ∘f +o ( 𝐴 × { ∅ } ) ) Fn 𝐴 )
41 elmapfn ⊢ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) → ℎ Fn 𝐴 )
42 elmapfn ⊢ ( ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) → ( 𝐴 × { ∅ } ) Fn 𝐴 )
43 41 42 anim12i ⊢ ( ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) → ( ℎ Fn 𝐴 ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) )
44 43 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( ℎ Fn 𝐴 ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) )
45 39 anim1i ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) )
46 fnfvof ⊢ ( ( ( ℎ Fn 𝐴 ∧ ( 𝐴 × { ∅ } ) Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( ℎ ∘f +o ( 𝐴 × { ∅ } ) ) ‘ 𝑎 ) = ( ( ℎ ‘ 𝑎 ) +o ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) ) )
47 44 45 46 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℎ ∘f +o ( 𝐴 × { ∅ } ) ) ‘ 𝑎 ) = ( ( ℎ ‘ 𝑎 ) +o ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) ) )
48 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
49 fvconst2g ⊢ ( ( ∅ ∈ ω ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) = ∅ )
50 13 48 49 sylancr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) = ∅ )
51 50 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℎ ‘ 𝑎 ) +o ( ( 𝐴 × { ∅ } ) ‘ 𝑎 ) ) = ( ( ℎ ‘ 𝑎 ) +o ∅ ) )
52 24 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → 𝐶 ∈ On )
53 52 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐶 ∈ On )
54 onss ⊢ ( 𝐶 ∈ On → 𝐶 ⊆ On )
55 53 54 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐶 ⊆ On )
56 31 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ℎ : 𝐴 ⟶ 𝐶 )
57 56 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ℎ ‘ 𝑎 ) ∈ 𝐶 )
58 55 57 sseldd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ℎ ‘ 𝑎 ) ∈ On )
59 oa0 ⊢ ( ( ℎ ‘ 𝑎 ) ∈ On → ( ( ℎ ‘ 𝑎 ) +o ∅ ) = ( ℎ ‘ 𝑎 ) )
60 58 59 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℎ ‘ 𝑎 ) +o ∅ ) = ( ℎ ‘ 𝑎 ) )
61 47 51 60 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℎ ∘f +o ( 𝐴 × { ∅ } ) ) ‘ 𝑎 ) = ( ℎ ‘ 𝑎 ) )
62 40 34 61 eqfnfvd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( ℎ ∘f +o ( 𝐴 × { ∅ } ) ) = ℎ )
63 30 62 eqtr2d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) ( 𝐴 × { ∅ } ) ) )
64 63 expr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ) → ( ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) → ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) ( 𝐴 × { ∅ } ) ) ) )
65 28 64 jcai ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ) → ( ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ∧ ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) ( 𝐴 × { ∅ } ) ) ) )
66 oveq2 ⊢ ( 𝑧 = ( 𝐴 × { ∅ } ) → ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) ( 𝐴 × { ∅ } ) ) )
67 66 rspceeqv ⊢ ( ( ( 𝐴 × { ∅ } ) ∈ ( 𝐶 ↑m 𝐴 ) ∧ ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) ( 𝐴 × { ∅ } ) ) ) → ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) )
68 65 67 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ) → ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) )
69 8 68 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ) → ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) ) )
70 oveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) )
71 70 eqeq2d ⊢ ( 𝑓 = ℎ → ( ℎ = ( 𝑓 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) ↔ ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) ) )
72 71 rexbidv ⊢ ( 𝑓 = ℎ → ( ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( 𝑓 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) ) )
73 72 rspcev ⊢ ( ( ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∧ ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( ℎ ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) ) → ∃ 𝑓 ∈ ( 𝐶 ↑m 𝐴 ) ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( 𝑓 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) )
74 69 73 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ) → ∃ 𝑓 ∈ ( 𝐶 ↑m 𝐴 ) ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( 𝑓 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) )
75 74 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ∀ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∃ 𝑓 ∈ ( 𝐶 ↑m 𝐴 ) ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( 𝑓 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) )
76 foov ⊢ ( ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) –onto→ ( 𝐶 ↑m 𝐴 ) ↔ ( ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ⟶ ( 𝐶 ↑m 𝐴 ) ∧ ∀ ℎ ∈ ( 𝐶 ↑m 𝐴 ) ∃ 𝑓 ∈ ( 𝐶 ↑m 𝐴 ) ∃ 𝑧 ∈ ( 𝐶 ↑m 𝐴 ) ℎ = ( 𝑓 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝑧 ) ) )
77 7 75 76 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) –onto→ ( 𝐶 ↑m 𝐴 ) )