Proof of Theorem imasaddvallemg
Step | Hyp | Ref
| Expression |
1 | | df-ov 5881 |
. 2
⊢ ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = ( ∙ ‘〈(𝐹‘𝑋), (𝐹‘𝑌)〉) |
2 | | imasaddf.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
3 | | imasaddf.e |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) |
4 | | imasaddflem.a |
. . . . . 6
⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
5 | | imasaddfnlemg.v |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ 𝑊) |
6 | | imasaddfnlemg.x |
. . . . . 6
⊢ (𝜑 → · ∈ 𝐶) |
7 | 2, 3, 4, 5, 6 | imasaddfnlemg 12741 |
. . . . 5
⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵)) |
8 | | fnfun 5315 |
. . . . 5
⊢ ( ∙ Fn
(𝐵 × 𝐵) → Fun ∙ ) |
9 | 7, 8 | syl 14 |
. . . 4
⊢ (𝜑 → Fun ∙ ) |
10 | 9 | 3ad2ant1 1018 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → Fun ∙ ) |
11 | | fveq2 5517 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑋 → (𝐹‘𝑝) = (𝐹‘𝑋)) |
12 | 11 | opeq1d 3786 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑋 → 〈(𝐹‘𝑝), (𝐹‘𝑌)〉 = 〈(𝐹‘𝑋), (𝐹‘𝑌)〉) |
13 | | fvoveq1 5901 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑋 → (𝐹‘(𝑝 · 𝑌)) = (𝐹‘(𝑋 · 𝑌))) |
14 | 12, 13 | opeq12d 3788 |
. . . . . . . . 9
⊢ (𝑝 = 𝑋 → 〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉 = 〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉) |
15 | 14 | sneqd 3607 |
. . . . . . . 8
⊢ (𝑝 = 𝑋 → {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉} = {〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉}) |
16 | 15 | ssiun2s 3932 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → {〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉} ⊆ ∪ 𝑝 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉}) |
17 | 16 | 3ad2ant2 1019 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉} ⊆ ∪ 𝑝 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉}) |
18 | | fveq2 5517 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑌 → (𝐹‘𝑞) = (𝐹‘𝑌)) |
19 | 18 | opeq2d 3787 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑌 → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑌)〉) |
20 | | oveq2 5886 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑌 → (𝑝 · 𝑞) = (𝑝 · 𝑌)) |
21 | 20 | fveq2d 5521 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑌 → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑝 · 𝑌))) |
22 | 19, 21 | opeq12d 3788 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑌 → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉) |
23 | 22 | sneqd 3607 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑌 → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} = {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉}) |
24 | 23 | ssiun2s 3932 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝑉 → {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉} ⊆ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
25 | 24 | ralrimivw 2551 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑉 → ∀𝑝 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉} ⊆ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
26 | | ss2iun 3903 |
. . . . . . . 8
⊢
(∀𝑝 ∈
𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉} ⊆ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → ∪ 𝑝 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉} ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
27 | 25, 26 | syl 14 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑉 → ∪
𝑝 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉} ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
28 | 27 | 3ad2ant3 1020 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∪
𝑝 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑌)〉, (𝐹‘(𝑝 · 𝑌))〉} ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
29 | 17, 28 | sstrd 3167 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉} ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
30 | 4 | 3ad2ant1 1018 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
31 | 29, 30 | sseqtrrd 3196 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉} ⊆ ∙ ) |
32 | | fof 5440 |
. . . . . . . . . . 11
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
33 | 2, 32 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
34 | 33 | 3ad2ant1 1018 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝐹:𝑉⟶𝐵) |
35 | 5 | 3ad2ant1 1018 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝑉 ∈ 𝑊) |
36 | 34, 35 | fexd 5749 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝐹 ∈ V) |
37 | | simp2 998 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
38 | | fvexg 5536 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ V) |
39 | 36, 37, 38 | syl2anc 411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐹‘𝑋) ∈ V) |
40 | | simp3 999 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ 𝑉) |
41 | | fvexg 5536 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ 𝑌 ∈ 𝑉) → (𝐹‘𝑌) ∈ V) |
42 | 36, 40, 41 | syl2anc 411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐹‘𝑌) ∈ V) |
43 | | opexg 4230 |
. . . . . . 7
⊢ (((𝐹‘𝑋) ∈ V ∧ (𝐹‘𝑌) ∈ V) → 〈(𝐹‘𝑋), (𝐹‘𝑌)〉 ∈ V) |
44 | 39, 42, 43 | syl2anc 411 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 〈(𝐹‘𝑋), (𝐹‘𝑌)〉 ∈ V) |
45 | 6 | 3ad2ant1 1018 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → · ∈ 𝐶) |
46 | | ovexg 5912 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ · ∈ 𝐶 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) ∈ V) |
47 | 37, 45, 40, 46 | syl3anc 1238 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) ∈ V) |
48 | | fvexg 5536 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ (𝑋 · 𝑌) ∈ V) → (𝐹‘(𝑋 · 𝑌)) ∈ V) |
49 | 36, 47, 48 | syl2anc 411 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐹‘(𝑋 · 𝑌)) ∈ V) |
50 | | opexg 4230 |
. . . . . 6
⊢
((〈(𝐹‘𝑋), (𝐹‘𝑌)〉 ∈ V ∧ (𝐹‘(𝑋 · 𝑌)) ∈ V) → 〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉 ∈ V) |
51 | 44, 49, 50 | syl2anc 411 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉 ∈ V) |
52 | | snssg 3728 |
. . . . 5
⊢
(〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉 ∈ V → (〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉 ∈ ∙ ↔
{〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉} ⊆ ∙ )) |
53 | 51, 52 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉 ∈ ∙ ↔
{〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉} ⊆ ∙ )) |
54 | 31, 53 | mpbird 167 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉 ∈ ∙ ) |
55 | | funopfv 5558 |
. . 3
⊢ (Fun
∙
→ (〈〈(𝐹‘𝑋), (𝐹‘𝑌)〉, (𝐹‘(𝑋 · 𝑌))〉 ∈ ∙ → ( ∙
‘〈(𝐹‘𝑋), (𝐹‘𝑌)〉) = (𝐹‘(𝑋 · 𝑌)))) |
56 | 10, 54, 55 | sylc 62 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ( ∙ ‘〈(𝐹‘𝑋), (𝐹‘𝑌)〉) = (𝐹‘(𝑋 · 𝑌))) |
57 | 1, 56 | eqtrid 2222 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) |