Step | Hyp | Ref
| Expression |
1 | | imasaddf.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
2 | | fof 5440 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
3 | 1, 2 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
4 | | imasaddfnlemg.v |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑉 ∈ 𝑊) |
5 | 3, 4 | fexd 5749 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
6 | | vex 2742 |
. . . . . . . . . . 11
⊢ 𝑝 ∈ V |
7 | | fvexg 5536 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ V ∧ 𝑝 ∈ V) → (𝐹‘𝑝) ∈ V) |
8 | 5, 6, 7 | sylancl 413 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑝) ∈ V) |
9 | | vex 2742 |
. . . . . . . . . . 11
⊢ 𝑞 ∈ V |
10 | | fvexg 5536 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ V ∧ 𝑞 ∈ V) → (𝐹‘𝑞) ∈ V) |
11 | 5, 9, 10 | sylancl 413 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑞) ∈ V) |
12 | | opexg 4230 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑝) ∈ V ∧ (𝐹‘𝑞) ∈ V) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ V) |
13 | 8, 11, 12 | syl2anc 411 |
. . . . . . . . 9
⊢ (𝜑 → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ V) |
14 | | imasaddfnlemg.x |
. . . . . . . . . . 11
⊢ (𝜑 → · ∈ 𝐶) |
15 | 9 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑞 ∈ V) |
16 | | ovexg 5912 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ V ∧ · ∈
𝐶 ∧ 𝑞 ∈ V) → (𝑝 · 𝑞) ∈ V) |
17 | 6, 14, 15, 16 | mp3an2i 1342 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑝 · 𝑞) ∈ V) |
18 | | fvexg 5536 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ V ∧ (𝑝 · 𝑞) ∈ V) → (𝐹‘(𝑝 · 𝑞)) ∈ V) |
19 | 5, 17, 18 | syl2anc 411 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝑝 · 𝑞)) ∈ V) |
20 | | relsnopg 4732 |
. . . . . . . . 9
⊢
((〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → Rel {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
21 | 13, 19, 20 | syl2anc 411 |
. . . . . . . 8
⊢ (𝜑 → Rel {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
22 | 21 | ralrimivw 2551 |
. . . . . . 7
⊢ (𝜑 → ∀𝑞 ∈ 𝑉 Rel {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
23 | | reliun 4749 |
. . . . . . 7
⊢ (Rel
∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∀𝑞 ∈ 𝑉 Rel {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
24 | 22, 23 | sylibr 134 |
. . . . . 6
⊢ (𝜑 → Rel ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
25 | 24 | ralrimivw 2551 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 Rel ∪
𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
26 | | reliun 4749 |
. . . . 5
⊢ (Rel
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∀𝑝 ∈ 𝑉 Rel ∪
𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
27 | 25, 26 | sylibr 134 |
. . . 4
⊢ (𝜑 → Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
28 | | imasaddflem.a |
. . . . 5
⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
29 | 28 | releqd 4712 |
. . . 4
⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
30 | 27, 29 | mpbird 167 |
. . 3
⊢ (𝜑 → Rel ∙ ) |
31 | | ffvelcdm 5652 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵) |
32 | | ffvelcdm 5652 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵) |
33 | 31, 32 | anim12dan 600 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵)) |
34 | 3, 33 | sylan 283 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵)) |
35 | | opelxpi 4660 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) |
36 | 34, 35 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (𝐵 × 𝐵)) |
37 | 19 | adantr 276 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝐹‘(𝑝 · 𝑞)) ∈ V) |
38 | 36, 37 | opelxpd 4661 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ((𝐵 × 𝐵) × V)) |
39 | 38 | snssd 3739 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
40 | 39 | anassrs 400 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
41 | 40 | iunssd 3934 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪
𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
42 | 41 | iunssd 3934 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ((𝐵 × 𝐵) × V)) |
43 | 28, 42 | eqsstrd 3193 |
. . . . . . 7
⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × V)) |
44 | | dmss 4828 |
. . . . . . 7
⊢ ( ∙
⊆ ((𝐵 × 𝐵) × V) → dom ∙
⊆ dom ((𝐵 ×
𝐵) ×
V)) |
45 | 43, 44 | syl 14 |
. . . . . 6
⊢ (𝜑 → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V)) |
46 | | vn0m 3436 |
. . . . . . 7
⊢
∃𝑤 𝑤 ∈ V |
47 | | dmxpm 4849 |
. . . . . . 7
⊢
(∃𝑤 𝑤 ∈ V → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
⊢ dom
((𝐵 × 𝐵) × V) = (𝐵 × 𝐵) |
49 | 45, 48 | sseqtrdi 3205 |
. . . . 5
⊢ (𝜑 → dom ∙ ⊆ (𝐵 × 𝐵)) |
50 | | forn 5443 |
. . . . . . 7
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) |
51 | 1, 50 | syl 14 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 = 𝐵) |
52 | 51 | sqxpeqd 4654 |
. . . . 5
⊢ (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵)) |
53 | 49, 52 | sseqtrrd 3196 |
. . . 4
⊢ (𝜑 → dom ∙ ⊆ (ran 𝐹 × ran 𝐹)) |
54 | 28 | eleq2d 2247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∙ ↔
〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
55 | 54 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∙ ↔
〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
56 | | df-br 4006 |
. . . . . . . . . . . 12
⊢
(〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∙ ) |
57 | | eliun 3892 |
. . . . . . . . . . . . 13
⊢
(〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∃𝑝 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
58 | | eliun 3892 |
. . . . . . . . . . . . . 14
⊢
(〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
59 | 58 | rexbii 2484 |
. . . . . . . . . . . . 13
⊢
(∃𝑝 ∈
𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
60 | 57, 59 | bitr2i 185 |
. . . . . . . . . . . 12
⊢
(∃𝑝 ∈
𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
61 | 55, 56, 60 | 3bitr4g 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉})) |
62 | | vex 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑎 ∈ V |
63 | | fvexg 5536 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ V ∧ 𝑎 ∈ V) → (𝐹‘𝑎) ∈ V) |
64 | 5, 62, 63 | sylancl 413 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹‘𝑎) ∈ V) |
65 | | vex 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑏 ∈ V |
66 | | fvexg 5536 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ V ∧ 𝑏 ∈ V) → (𝐹‘𝑏) ∈ V) |
67 | 5, 65, 66 | sylancl 413 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹‘𝑏) ∈ V) |
68 | | opexg 4230 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑎) ∈ V ∧ (𝐹‘𝑏) ∈ V) → 〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∈ V) |
69 | 64, 67, 68 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∈ V) |
70 | | vex 2742 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V |
71 | | opexg 4230 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∈ V ∧ 𝑤 ∈ V) → 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ V) |
72 | 69, 70, 71 | sylancl 413 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ V) |
73 | | elsng 3609 |
. . . . . . . . . . . . . . . 16
⊢
(〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ V → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉)) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉)) |
75 | 74 | 3ad2ant1 1018 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ↔ 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉)) |
76 | | opthg 4240 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∈ V ∧ 𝑤 ∈ V) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ↔ (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))) |
77 | 69, 70, 76 | sylancl 413 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ↔ (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))) |
78 | 77 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ↔ (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))) |
79 | | opthg 4240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘𝑎) ∈ V ∧ (𝐹‘𝑏) ∈ V) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)))) |
80 | 64, 67, 79 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)))) |
81 | 80 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)))) |
82 | | imasaddf.e |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) |
83 | 81, 82 | sylbid 150 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) |
84 | | eqeq2 2187 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞)))) |
85 | 84 | biimprd 158 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
86 | 83, 85 | syl6 33 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))) |
87 | 86 | impd 254 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((〈(𝐹‘𝑎), (𝐹‘𝑏)〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
88 | 78, 87 | sylbid 150 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 = 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
89 | 75, 88 | sylbid 150 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
90 | 89 | 3expa 1203 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
91 | 90 | rexlimdvva 2602 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 〈〈(𝐹‘𝑎), (𝐹‘𝑏)〉, 𝑤〉 ∈ {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
92 | 61, 91 | sylbid 150 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
93 | 92 | alrimiv 1874 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑤(〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏)))) |
94 | | mo2icl 2918 |
. . . . . . . . 9
⊢
(∀𝑤(〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤) |
95 | 93, 94 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤) |
96 | 95 | ralrimivva 2559 |
. . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤) |
97 | | fofn 5442 |
. . . . . . . . . 10
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉) |
98 | 1, 97 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑉) |
99 | | opeq2 3781 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘𝑏) → 〈(𝐹‘𝑎), 𝑧〉 = 〈(𝐹‘𝑎), (𝐹‘𝑏)〉) |
100 | 99 | breq1d 4015 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑏) → (〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ 〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
101 | 100 | mobidv 2062 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘𝑏) → (∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
102 | 101 | ralrn 5657 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
103 | 98, 102 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
104 | 103 | ralbidv 2477 |
. . . . . . 7
⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤〈(𝐹‘𝑎), (𝐹‘𝑏)〉 ∙ 𝑤)) |
105 | 96, 104 | mpbird 167 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤) |
106 | | opeq1 3780 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑎) → 〈𝑦, 𝑧〉 = 〈(𝐹‘𝑎), 𝑧〉) |
107 | 106 | breq1d 4015 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑎) → (〈𝑦, 𝑧〉 ∙ 𝑤 ↔ 〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
108 | 107 | mobidv 2062 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑎) → (∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
109 | 108 | ralbidv 2477 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
110 | 109 | ralrn 5657 |
. . . . . . 7
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
111 | 98, 110 | syl 14 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤〈(𝐹‘𝑎), 𝑧〉 ∙ 𝑤)) |
112 | 105, 111 | mpbird 167 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤) |
113 | | breq1 4008 |
. . . . . . 7
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∙ 𝑤 ↔ 〈𝑦, 𝑧〉 ∙ 𝑤)) |
114 | 113 | mobidv 2062 |
. . . . . 6
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (∃*𝑤 𝑥 ∙ 𝑤 ↔ ∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤)) |
115 | 114 | ralxp 4772 |
. . . . 5
⊢
(∀𝑥 ∈
(ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤〈𝑦, 𝑧〉 ∙ 𝑤) |
116 | 112, 115 | sylibr 134 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤) |
117 | | ssralv 3221 |
. . . 4
⊢ (dom
∙
⊆ (ran 𝐹 × ran
𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
118 | 53, 116, 117 | sylc 62 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤) |
119 | | dffun7 5245 |
. . 3
⊢ (Fun
∙
↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)) |
120 | 30, 118, 119 | sylanbrc 417 |
. 2
⊢ (𝜑 → Fun ∙ ) |
121 | | eqimss2 3212 |
. . . . . . . . . . 11
⊢ ( ∙ =
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
122 | 28, 121 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
123 | | iunss 3929 |
. . . . . . . . . 10
⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ↔
∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
124 | 122, 123 | sylib 122 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
125 | | iunss 3929 |
. . . . . . . . . . 11
⊢ (∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ↔
∀𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ ) |
126 | | opexg 4230 |
. . . . . . . . . . . . . . 15
⊢
((〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ V) |
127 | 13, 19, 126 | syl2anc 411 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ V) |
128 | | snssg 3728 |
. . . . . . . . . . . . . 14
⊢
(〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ V → (〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ∙ ↔
{〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ )) |
129 | 127, 128 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ∙ ↔
{〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ )) |
130 | | opeldmg 4834 |
. . . . . . . . . . . . . 14
⊢
((〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → (〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ∙ → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
131 | 13, 19, 130 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉 ∈ ∙ → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
132 | 129, 131 | sylbird 170 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
133 | 132 | ralimdv 2545 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ →
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
134 | 125, 133 | biimtrid 152 |
. . . . . . . . . 10
⊢ (𝜑 → (∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ →
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
135 | 134 | ralimdv 2545 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ⊆ ∙ →
∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
136 | 124, 135 | mpd 13 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ ) |
137 | | opeq2 3781 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘𝑞) → 〈(𝐹‘𝑝), 𝑧〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉) |
138 | 137 | eleq1d 2246 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑞) → (〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔ 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
139 | 138 | ralrn 5657 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
140 | 98, 139 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔
∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
141 | 140 | ralbidv 2477 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ dom ∙ )) |
142 | 136, 141 | mpbird 167 |
. . . . . . 7
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ ) |
143 | | opeq1 3780 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑝) → 〈𝑦, 𝑧〉 = 〈(𝐹‘𝑝), 𝑧〉) |
144 | 143 | eleq1d 2246 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑝) → (〈𝑦, 𝑧〉 ∈ dom ∙ ↔ 〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
145 | 144 | ralbidv 2477 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑝) → (∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ↔
∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
146 | 145 | ralrn 5657 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
147 | 98, 146 | syl 14 |
. . . . . . 7
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ↔
∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹〈(𝐹‘𝑝), 𝑧〉 ∈ dom ∙ )) |
148 | 142, 147 | mpbird 167 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ) |
149 | | eleq1 2240 |
. . . . . . 7
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ dom ∙ ↔ 〈𝑦, 𝑧〉 ∈ dom ∙ )) |
150 | 149 | ralxp 4772 |
. . . . . 6
⊢
(∀𝑥 ∈
(ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ↔
∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹〈𝑦, 𝑧〉 ∈ dom ∙ ) |
151 | 148, 150 | sylibr 134 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ) |
152 | | dfss3 3147 |
. . . . 5
⊢ ((ran
𝐹 × ran 𝐹) ⊆ dom ∙ ↔
∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ) |
153 | 151, 152 | sylibr 134 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom ∙ ) |
154 | 52, 153 | eqsstrrd 3194 |
. . 3
⊢ (𝜑 → (𝐵 × 𝐵) ⊆ dom ∙ ) |
155 | 49, 154 | eqssd 3174 |
. 2
⊢ (𝜑 → dom ∙ = (𝐵 × 𝐵)) |
156 | | df-fn 5221 |
. 2
⊢ ( ∙ Fn
(𝐵 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ =
(𝐵 × 𝐵))) |
157 | 120, 155,
156 | sylanbrc 417 |
1
⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵)) |