Proof of Theorem imasaddflem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | imasaddf.f | . . 3
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) | 
| 2 |  | imasaddf.e | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) | 
| 3 |  | imasaddflem.a | . . 3
⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) | 
| 4 | 1, 2, 3 | imasaddfnlem 17573 | . 2
⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵)) | 
| 5 |  | fof 6820 | . . . . . . . . . 10
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) | 
| 6 | 1, 5 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) | 
| 7 |  | ffvelcdm 7101 | . . . . . . . . . . 11
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵) | 
| 8 |  | ffvelcdm 7101 | . . . . . . . . . . 11
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵) | 
| 9 | 7, 8 | anim12dan 619 | . . . . . . . . . 10
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵)) | 
| 10 |  | opelxpi 5722 | . . . . . . . . . 10
⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . 9
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) | 
| 12 | 6, 11 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) | 
| 13 |  | imasaddflem.c | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) | 
| 14 |  | ffvelcdm 7101 | . . . . . . . . 9
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 · 𝑞) ∈ 𝑉) → (𝐹‘(𝑝 · 𝑞)) ∈ 𝐵) | 
| 15 | 6, 13, 14 | syl2an2r 685 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝐹‘(𝑝 · 𝑞)) ∈ 𝐵) | 
| 16 | 12, 15 | opelxpd 5724 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ((𝐵 × 𝐵) × 𝐵)) | 
| 17 | 16 | snssd 4809 | . . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) | 
| 18 | 17 | anassrs 467 | . . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) | 
| 19 | 18 | iunssd 5050 | . . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪
𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) | 
| 20 | 19 | iunssd 5050 | . . 3
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) | 
| 21 | 3, 20 | eqsstrd 4018 | . 2
⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × 𝐵)) | 
| 22 |  | dff2 7119 | . 2
⊢ ( ∙
:(𝐵 × 𝐵)⟶𝐵 ↔ ( ∙ Fn (𝐵 × 𝐵) ∧ ∙ ⊆ ((𝐵 × 𝐵) × 𝐵))) | 
| 23 | 4, 21, 22 | sylanbrc 583 | 1
⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵) |