| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) | 
| 2 |  | inidm 4226 | . . . . . 6
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 3 | 2 | eqcomi 2745 | . . . . 5
⊢ 𝐴 = (𝐴 ∩ 𝐴) | 
| 4 | 3 | a1i 11 | . . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 = (𝐴 ∩ 𝐴)) | 
| 5 | 1, 1, 4 | 3jca 1128 | . . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 = (𝐴 ∩ 𝐴))) | 
| 6 |  | ofoaf 43373 | . . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 = (𝐴 ∩ 𝐴)) ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ( ∘f
+o ↾ ((𝐶
↑m 𝐴)
× (𝐶
↑m 𝐴))):((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐴))⟶(𝐶 ↑m 𝐴)) | 
| 7 | 5, 6 | sylan 580 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ( ∘f
+o ↾ ((𝐶
↑m 𝐴)
× (𝐶
↑m 𝐴))):((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐴))⟶(𝐶 ↑m 𝐴)) | 
| 8 |  | simpr 484 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ ℎ ∈ (𝐶 ↑m 𝐴)) → ℎ ∈ (𝐶 ↑m 𝐴)) | 
| 9 |  | omelon 9687 | . . . . . . . . . . . . . . 15
⊢ ω
∈ On | 
| 10 | 9 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → ω ∈
On) | 
| 11 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → 𝐵 ∈ On) | 
| 12 | 10, 11 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → (ω ∈
On ∧ 𝐵 ∈
On)) | 
| 13 |  | peano1 7911 | . . . . . . . . . . . . 13
⊢ ∅
∈ ω | 
| 14 |  | oen0 8625 | . . . . . . . . . . . . 13
⊢
(((ω ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝐵)) | 
| 15 | 12, 13, 14 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → ∅ ∈
(ω ↑o 𝐵)) | 
| 16 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → 𝐶 = (ω ↑o
𝐵)) | 
| 17 | 15, 16 | eleqtrrd 2843 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → ∅ ∈
𝐶) | 
| 18 |  | fconst6g 6796 | . . . . . . . . . . 11
⊢ (∅
∈ 𝐶 → (𝐴 × {∅}):𝐴⟶𝐶) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → (𝐴 × {∅}):𝐴⟶𝐶) | 
| 20 | 19 | adantl 481 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → (𝐴 × {∅}):𝐴⟶𝐶) | 
| 21 |  | oecl 8576 | . . . . . . . . . . . . 13
⊢ ((ω
∈ On ∧ 𝐵 ∈
On) → (ω ↑o 𝐵) ∈ On) | 
| 22 | 9, 11, 21 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → (ω
↑o 𝐵)
∈ On) | 
| 23 | 16, 22 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 = (ω ↑o
𝐵)) → 𝐶 ∈ On) | 
| 24 | 23 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → 𝐶 ∈ On) | 
| 25 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → 𝐴 ∈ 𝑉) | 
| 26 | 24, 25 | elmapd 8881 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ((𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴) ↔ (𝐴 × {∅}):𝐴⟶𝐶)) | 
| 27 | 20, 26 | mpbird 257 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) | 
| 28 | 27 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ ℎ ∈ (𝐶 ↑m 𝐴)) → (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) | 
| 29 |  | ovres 7600 | . . . . . . . . . 10
⊢ ((ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) → (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))(𝐴 × {∅})) = (ℎ ∘f +o (𝐴 ×
{∅}))) | 
| 30 | 29 | adantl 481 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))(𝐴 × {∅})) = (ℎ ∘f +o (𝐴 ×
{∅}))) | 
| 31 |  | elmapi 8890 | . . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝐶 ↑m 𝐴) → ℎ:𝐴⟶𝐶) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) → ℎ:𝐴⟶𝐶) | 
| 33 | 32 | ffnd 6736 | . . . . . . . . . . . 12
⊢ ((ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) → ℎ Fn 𝐴) | 
| 34 | 33 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → ℎ Fn 𝐴) | 
| 35 |  | elmapi 8890 | . . . . . . . . . . . . . 14
⊢ ((𝐴 × {∅}) ∈
(𝐶 ↑m 𝐴) → (𝐴 × {∅}):𝐴⟶𝐶) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) → (𝐴 × {∅}):𝐴⟶𝐶) | 
| 37 | 36 | ffnd 6736 | . . . . . . . . . . . 12
⊢ ((ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) → (𝐴 × {∅}) Fn 𝐴) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → (𝐴 × {∅}) Fn 𝐴) | 
| 39 | 25 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → 𝐴 ∈ 𝑉) | 
| 40 | 34, 38, 39, 39, 2 | offn 7711 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → (ℎ ∘f +o (𝐴 × {∅})) Fn 𝐴) | 
| 41 |  | elmapfn 8906 | . . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝐶 ↑m 𝐴) → ℎ Fn 𝐴) | 
| 42 |  | elmapfn 8906 | . . . . . . . . . . . . . 14
⊢ ((𝐴 × {∅}) ∈
(𝐶 ↑m 𝐴) → (𝐴 × {∅}) Fn 𝐴) | 
| 43 | 41, 42 | anim12i 613 | . . . . . . . . . . . . 13
⊢ ((ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴)) → (ℎ Fn 𝐴 ∧ (𝐴 × {∅}) Fn 𝐴)) | 
| 44 | 43 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → (ℎ Fn 𝐴 ∧ (𝐴 × {∅}) Fn 𝐴)) | 
| 45 | 39 | anim1i 615 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → (𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴)) | 
| 46 |  | fnfvof 7715 | . . . . . . . . . . . 12
⊢ (((ℎ Fn 𝐴 ∧ (𝐴 × {∅}) Fn 𝐴) ∧ (𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴)) → ((ℎ ∘f +o (𝐴 × {∅}))‘𝑎) = ((ℎ‘𝑎) +o ((𝐴 × {∅})‘𝑎))) | 
| 47 | 44, 45, 46 | syl2an2r 685 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → ((ℎ ∘f +o (𝐴 × {∅}))‘𝑎) = ((ℎ‘𝑎) +o ((𝐴 × {∅})‘𝑎))) | 
| 48 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) | 
| 49 |  | fvconst2g 7223 | . . . . . . . . . . . . 13
⊢ ((∅
∈ ω ∧ 𝑎
∈ 𝐴) → ((𝐴 × {∅})‘𝑎) = ∅) | 
| 50 | 13, 48, 49 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → ((𝐴 × {∅})‘𝑎) = ∅) | 
| 51 | 50 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → ((ℎ‘𝑎) +o ((𝐴 × {∅})‘𝑎)) = ((ℎ‘𝑎) +o ∅)) | 
| 52 | 24 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → 𝐶 ∈ On) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ On) | 
| 54 |  | onss 7806 | . . . . . . . . . . . . . 14
⊢ (𝐶 ∈ On → 𝐶 ⊆ On) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → 𝐶 ⊆ On) | 
| 56 | 31 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → ℎ:𝐴⟶𝐶) | 
| 57 | 56 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → (ℎ‘𝑎) ∈ 𝐶) | 
| 58 | 55, 57 | sseldd 3983 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → (ℎ‘𝑎) ∈ On) | 
| 59 |  | oa0 8555 | . . . . . . . . . . . 12
⊢ ((ℎ‘𝑎) ∈ On → ((ℎ‘𝑎) +o ∅) = (ℎ‘𝑎)) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → ((ℎ‘𝑎) +o ∅) = (ℎ‘𝑎)) | 
| 61 | 47, 51, 60 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) ∧ 𝑎 ∈ 𝐴) → ((ℎ ∘f +o (𝐴 × {∅}))‘𝑎) = (ℎ‘𝑎)) | 
| 62 | 40, 34, 61 | eqfnfvd 7053 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → (ℎ ∘f +o (𝐴 × {∅})) = ℎ) | 
| 63 | 30, 62 | eqtr2d 2777 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (ℎ ∈ (𝐶 ↑m 𝐴) ∧ (𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴))) → ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))(𝐴 × {∅}))) | 
| 64 | 63 | expr 456 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ ℎ ∈ (𝐶 ↑m 𝐴)) → ((𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴) → ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))(𝐴 × {∅})))) | 
| 65 | 28, 64 | jcai 516 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ ℎ ∈ (𝐶 ↑m 𝐴)) → ((𝐴 × {∅}) ∈ (𝐶 ↑m 𝐴) ∧ ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))(𝐴 × {∅})))) | 
| 66 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑧 = (𝐴 × {∅}) → (ℎ( ∘f
+o ↾ ((𝐶
↑m 𝐴)
× (𝐶
↑m 𝐴)))𝑧) = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))(𝐴 × {∅}))) | 
| 67 | 66 | rspceeqv 3644 | . . . . . 6
⊢ (((𝐴 × {∅}) ∈
(𝐶 ↑m 𝐴) ∧ ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))(𝐴 × {∅}))) → ∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧)) | 
| 68 | 65, 67 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ ℎ ∈ (𝐶 ↑m 𝐴)) → ∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧)) | 
| 69 | 8, 68 | jca 511 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ ℎ ∈ (𝐶 ↑m 𝐴)) → (ℎ ∈ (𝐶 ↑m 𝐴) ∧ ∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧))) | 
| 70 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑓 = ℎ → (𝑓( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧) = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧)) | 
| 71 | 70 | eqeq2d 2747 | . . . . . 6
⊢ (𝑓 = ℎ → (ℎ = (𝑓( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧) ↔ ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧))) | 
| 72 | 71 | rexbidv 3178 | . . . . 5
⊢ (𝑓 = ℎ → (∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (𝑓( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧) ↔ ∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧))) | 
| 73 | 72 | rspcev 3621 | . . . 4
⊢ ((ℎ ∈ (𝐶 ↑m 𝐴) ∧ ∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (ℎ( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧)) → ∃𝑓 ∈ (𝐶 ↑m 𝐴)∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (𝑓( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧)) | 
| 74 | 69, 73 | syl 17 | . . 3
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ ℎ ∈ (𝐶 ↑m 𝐴)) → ∃𝑓 ∈ (𝐶 ↑m 𝐴)∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (𝑓( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧)) | 
| 75 | 74 | ralrimiva 3145 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ∀ℎ ∈ (𝐶 ↑m 𝐴)∃𝑓 ∈ (𝐶 ↑m 𝐴)∃𝑧 ∈ (𝐶 ↑m 𝐴)ℎ = (𝑓( ∘f +o ↾
((𝐶 ↑m
𝐴) × (𝐶 ↑m 𝐴)))𝑧)) | 
| 76 |  | foov 7608 | . 2
⊢ ((
∘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 583 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ( ∘f
+o ↾ ((𝐶
↑m 𝐴)
× (𝐶
↑m 𝐴))):((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐴))–onto→(𝐶 ↑m 𝐴)) |