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 16011 |
. 2
⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵)) |
5 | | fof 6028 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
6 | 1, 5 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
7 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵) |
8 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵) |
9 | 7, 8 | anim12dan 878 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵)) |
10 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) |
12 | 6, 11 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) |
13 | | imasaddflem.c |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) |
14 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 · 𝑞) ∈ 𝑉) → (𝐹‘(𝑝 · 𝑞)) ∈ 𝐵) |
15 | 6, 14 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 · 𝑞) ∈ 𝑉) → (𝐹‘(𝑝 · 𝑞)) ∈ 𝐵) |
16 | 13, 15 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝐹‘(𝑝 · 𝑞)) ∈ 𝐵) |
17 | | opelxpi 5072 |
. . . . . . . . . 10
⊢
((〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ 𝐵) → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ((𝐵 × 𝐵) × 𝐵)) |
18 | 12, 16, 17 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ((𝐵 × 𝐵) × 𝐵)) |
19 | 18 | snssd 4281 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
20 | 19 | anassrs 678 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
21 | 20 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∀𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
22 | | iunss 4497 |
. . . . . 6
⊢ (∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵) ↔ ∀𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
23 | 21, 22 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪
𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
24 | 23 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
25 | | iunss 4497 |
. . . 4
⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵) ↔ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
26 | 24, 25 | sylibr 223 |
. . 3
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × 𝐵)) |
27 | 3, 26 | eqsstrd 3602 |
. 2
⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × 𝐵)) |
28 | | dff2 6279 |
. 2
⊢ ( ∙
:(𝐵 × 𝐵)⟶𝐵 ↔ ( ∙ Fn (𝐵 × 𝐵) ∧ ∙ ⊆ ((𝐵 × 𝐵) × 𝐵))) |
29 | 4, 27, 28 | sylanbrc 695 |
1
⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵) |