Step | Hyp | Ref
| Expression |
1 | | opex 5348 |
. . . . . . . . 9
⊢
〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ V |
2 | | fvex 6730 |
. . . . . . . . 9
⊢ (𝐹‘(𝑝 · 𝑞)) ∈ V |
3 | 1, 2 | relsnop 5675 |
. . . . . . . 8
⊢ Rel
{〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} |
4 | 3 | rgenw 3073 |
. . . . . . 7
⊢
∀𝑞 ∈
𝑉 Rel {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} |
5 | | reliun 5686 |
. . . . . . 7
⊢ (Rel
∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∀𝑞 ∈ 𝑉 Rel {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
6 | 4, 5 | mpbir 234 |
. . . . . 6
⊢ Rel
∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} |
7 | 6 | rgenw 3073 |
. . . . 5
⊢
∀𝑝 ∈
𝑉 Rel ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} |
8 | | reliun 5686 |
. . . . 5
⊢ (Rel
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∀𝑝 ∈ 𝑉 Rel ∪
𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
9 | 7, 8 | mpbir 234 |
. . . 4
⊢ Rel
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} |
10 | | imasaddflem.a |
. . . . 5
⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
11 | 10 | releqd 5650 |
. . . 4
⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
12 | 9, 11 | mpbiri 261 |
. . 3
⊢ (𝜑 → Rel ∙ ) |
13 | | imasaddf.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
14 | | fof 6633 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
16 | | ffvelrn 6902 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵) |
17 | | ffvelrn 6902 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵) |
18 | 16, 17 | anim12dan 622 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵)) |
19 | 15, 18 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵)) |
20 | | opelxpi 5588 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) |
22 | | opelxpi 5588 |
. . . . . . . . . . . . 13
⊢
((〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ((𝐵 × 𝐵) × V)) |
23 | 21, 2, 22 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ((𝐵 × 𝐵) × V)) |
24 | 23 | snssd 4722 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
25 | 24 | anassrs 471 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
26 | 25 | iunssd 4959 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪
𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
27 | 26 | iunssd 4959 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
28 | 10, 27 | eqsstrd 3939 |
. . . . . . 7
⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × V)) |
29 | | dmss 5771 |
. . . . . . 7
⊢ ( ∙
⊆ ((𝐵 × 𝐵) × V) → dom ∙
⊆ dom ((𝐵 ×
𝐵) ×
V)) |
30 | 28, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V)) |
31 | | vn0 4253 |
. . . . . . 7
⊢ V ≠
∅ |
32 | | dmxp 5798 |
. . . . . . 7
⊢ (V ≠
∅ → dom ((𝐵
× 𝐵) × V) =
(𝐵 × 𝐵)) |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
⊢ dom
((𝐵 × 𝐵) × V) = (𝐵 × 𝐵) |
34 | 30, 33 | sseqtrdi 3951 |
. . . . 5
⊢ (𝜑 → dom ∙ ⊆ (𝐵 × 𝐵)) |
35 | | forn 6636 |
. . . . . . 7
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) |
36 | 13, 35 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 = 𝐵) |
37 | 36 | sqxpeqd 5583 |
. . . . 5
⊢ (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵)) |
38 | 34, 37 | sseqtrrd 3942 |
. . . 4
⊢ (𝜑 → dom ∙ ⊆ (ran 𝐹 × ran 𝐹)) |
39 | 10 | eleq2d 2823 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∙ ↔
〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
40 | 39 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∙ ↔
〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
41 | | df-br 5054 |
. . . . . . . . . . . 12
⊢
(〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∙ ) |
42 | | eliun 4908 |
. . . . . . . . . . . . 13
⊢
(〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∃𝑝 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
43 | | eliun 4908 |
. . . . . . . . . . . . . 14
⊢
(〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
44 | 43 | rexbii 3170 |
. . . . . . . . . . . . 13
⊢
(∃𝑝 ∈
𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
45 | 42, 44 | bitr2i 279 |
. . . . . . . . . . . 12
⊢
(∃𝑝 ∈
𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
46 | 40, 41, 45 | 3bitr4g 317 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
47 | | opex 5348 |
. . . . . . . . . . . . . . 15
⊢
〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ V |
48 | 47 | elsn 4556 |
. . . . . . . . . . . . . 14
⊢
(〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉) |
49 | | opex 5348 |
. . . . . . . . . . . . . . . 16
⊢
〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∈ V |
50 | | vex 3412 |
. . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V |
51 | 49, 50 | opth 5360 |
. . . . . . . . . . . . . . 15
⊢
(〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ↔ (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞)))) |
52 | | fvex 6730 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹‘𝑎) ∈ V |
53 | | fvex 6730 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹‘𝑏) ∈ V |
54 | 52, 53 | opth 5360 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞))) |
55 | | imasaddf.e |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) |
56 | 54, 55 | syl5bi 245 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) |
57 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞)))) |
58 | 57 | biimprd 251 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
59 | 56, 58 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))) |
60 | 59 | impd 414 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
61 | 51, 60 | syl5bi 245 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
62 | 48, 61 | syl5bi 245 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
63 | 62 | 3expa 1120 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
64 | 63 | rexlimdvva 3213 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
65 | 46, 64 | sylbid 243 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
66 | 65 | alrimiv 1935 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑤(〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
67 | | mo2icl 3627 |
. . . . . . . . 9
⊢
(∀𝑤(〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤) |
69 | 68 | ralrimivva 3112 |
. . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤) |
70 | | fofn 6635 |
. . . . . . . . . 10
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉) |
71 | 13, 70 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑉) |
72 | | opeq2 4785 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘𝑏) → 〈(𝐹‘𝑎), 𝑧〉 = 〈(𝐹‘𝑎), (𝐹‘𝑏)〉) |
73 | 72 | breq1d 5063 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑏) → (〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ 〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
74 | 73 | mobidv 2548 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘𝑏) → (∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
75 | 74 | ralrn 6907 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
76 | 71, 75 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
77 | 76 | ralbidv 3118 |
. . . . . . 7
⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
78 | 69, 77 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤) |
79 | | opeq1 4784 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑎) → 〈𝑦, 𝑧〉 = 〈(𝐹‘𝑎), 𝑧〉) |
80 | 79 | breq1d 5063 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑎) → (〈𝑦, 𝑧〉 ∙ 𝑤 ↔ 〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
81 | 80 | mobidv 2548 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑎) → (∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
82 | 81 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
83 | 82 | ralrn 6907 |
. . . . . . 7
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
84 | 71, 83 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
85 | 78, 84 | mpbird 260 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤) |
86 | | breq1 5056 |
. . . . . . 7
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∙ 𝑤 ↔ 〈𝑦, 𝑧〉 ∙ 𝑤)) |
87 | 86 | mobidv 2548 |
. . . . . 6
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (∃*𝑤 𝑥 ∙ 𝑤 ↔ ∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤)) |
88 | 87 | ralxp 5710 |
. . . . 5
⊢
(∀𝑥 ∈
(ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤) |
89 | 85, 88 | sylibr 237 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤) |
90 | | ssralv 3967 |
. . . 4
⊢ (dom
∙
⊆ (ran 𝐹 × ran
𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
91 | 38, 89, 90 | sylc 65 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤) |
92 | | dffun7 6407 |
. . 3
⊢ (Fun
∙
↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
93 | 12, 91, 92 | sylanbrc 586 |
. 2
⊢ (𝜑 → Fun ∙ ) |
94 | | eqimss2 3958 |
. . . . . . . . . . 11
⊢ ( ∙ =
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
95 | 10, 94 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
96 | | iunss 4954 |
. . . . . . . . . 10
⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ↔
∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
97 | 95, 96 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
98 | | iunss 4954 |
. . . . . . . . . . 11
⊢ (∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ↔
∀𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
99 | | opex 5348 |
. . . . . . . . . . . . . 14
⊢
〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ V |
100 | 99 | snss 4699 |
. . . . . . . . . . . . 13
⊢
(〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ∙ ↔
{〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
101 | 1, 2 | opeldm 5776 |
. . . . . . . . . . . . 13
⊢
(〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ∙ → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ ) |
102 | 100, 101 | sylbir 238 |
. . . . . . . . . . . 12
⊢
({〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ ) |
103 | 102 | ralimi 3083 |
. . . . . . . . . . 11
⊢
(∀𝑞 ∈
𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ →
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ ) |
104 | 98, 103 | sylbi 220 |
. . . . . . . . . 10
⊢ (∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ →
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ ) |
105 | 104 | ralimi 3083 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ →
∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ ) |
106 | 97, 105 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ ) |
107 | | opeq2 4785 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘𝑞) → 〈(𝐹‘𝑝), 𝑧〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉) |
108 | 107 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑞) → (〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔ 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
109 | 108 | ralrn 6907 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
110 | 71, 109 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
111 | 110 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
112 | 106, 111 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ) |
113 | | opeq1 4784 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑝) → 〈𝑦, 𝑧〉 = 〈(𝐹‘𝑝), 𝑧〉) |
114 | 113 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑝) → (〈𝑦, 𝑧〉 ∈ dom ∙ ↔ 〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
115 | 114 | ralbidv 3118 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑝) → (∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ↔
∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
116 | 115 | ralrn 6907 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
117 | 71, 116 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
118 | 112, 117 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ) |
119 | | eleq1 2825 |
. . . . . . 7
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ dom ∙ ↔ 〈𝑦, 𝑧〉 ∈ dom ∙ )) |
120 | 119 | ralxp 5710 |
. . . . . 6
⊢
(∀𝑥 ∈
(ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ↔
∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ) |
121 | 118, 120 | sylibr 237 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ) |
122 | | dfss3 3888 |
. . . . 5
⊢ ((ran
𝐹 × ran 𝐹) ⊆ dom ∙ ↔
∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ) |
123 | 121, 122 | sylibr 237 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom ∙ ) |
124 | 37, 123 | eqsstrrd 3940 |
. . 3
⊢ (𝜑 → (𝐵 × 𝐵) ⊆ dom ∙ ) |
125 | 34, 124 | eqssd 3918 |
. 2
⊢ (𝜑 → dom ∙ = (𝐵 × 𝐵)) |
126 | | df-fn 6383 |
. 2
⊢ ( ∙ Fn
(𝐵 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ =
(𝐵 × 𝐵))) |
127 | 93, 125, 126 | sylanbrc 586 |
1
⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵)) |