Step | Hyp | Ref
| Expression |
1 | | relco 5633 |
. 2
⊢ Rel
(𝐺 ∘ 𝐹) |
2 | | mptrel 5248 |
. 2
⊢ Rel
(𝑥 ∈ 𝐴 ↦ 𝑇) |
3 | | fmptco.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) |
4 | | fmptco.1 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵) |
5 | 3, 4 | fmpt3d 6386 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
6 | 5 | ffund 6049 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) |
7 | | funbrfv 6234 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢)) |
8 | 7 | imp 445 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢) |
9 | 6, 8 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢) |
10 | 9 | eqcomd 2628 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧)) |
11 | 10 | a1d 25 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧))) |
12 | 11 | expimpd 629 |
. . . . . 6
⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧))) |
13 | 12 | pm4.71rd 667 |
. . . . 5
⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)))) |
14 | 13 | exbidv 1850 |
. . . 4
⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)))) |
15 | | fvex 6201 |
. . . . . 6
⊢ (𝐹‘𝑧) ∈ V |
16 | | breq2 4657 |
. . . . . . 7
⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧))) |
17 | | breq1 4656 |
. . . . . . 7
⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤)) |
18 | 16, 17 | anbi12d 747 |
. . . . . 6
⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤))) |
19 | 15, 18 | ceqsexv 3242 |
. . . . 5
⊢
(∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)) |
20 | | funfvbrb 6330 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧))) |
21 | 6, 20 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧))) |
22 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
23 | 5, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
24 | 23 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴)) |
25 | 21, 24 | bitr3d 270 |
. . . . . . 7
⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴)) |
26 | 3 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)) |
27 | | fmptco.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
28 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → 𝑤 = 𝑤) |
29 | 26, 27, 28 | breq123d 4667 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)) |
30 | 25, 29 | anbi12d 747 |
. . . . . 6
⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))) |
31 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑧 |
32 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜑 |
33 | | nffvmpt1 6199 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧) |
34 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆) |
35 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑤 |
36 | 33, 34, 35 | nfbr 4699 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 |
37 | | nfcsb1v 3549 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇 |
38 | 37 | nfeq2 2780 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇 |
39 | 36, 38 | nfbi 1833 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇) |
40 | 32, 39 | nfim 1825 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
41 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)) |
42 | 41 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)) |
43 | | csbeq1a 3542 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇) |
44 | 43 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
45 | 42, 44 | bibi12d 335 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
46 | 45 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))) |
47 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑤 ∈ V |
48 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅) |
49 | 48 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵)) |
50 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑤 → 𝑢 = 𝑤) |
51 | | fmptco.4 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) |
52 | 50, 51 | eqeqan12rd 2640 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇)) |
53 | 49, 52 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
54 | | df-mpt 4730 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {〈𝑦, 𝑢〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)} |
55 | 53, 54 | brabga 4989 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
56 | 4, 47, 55 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
57 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴) |
58 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
59 | 58 | fvmpt2 6291 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
60 | 57, 4, 59 | syl2an2 875 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
61 | 60 | breq1d 4663 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)) |
62 | 4 | biantrurd 529 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
63 | 56, 61, 62 | 3bitr4d 300 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) |
64 | 63 | expcom 451 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))) |
65 | 31, 40, 46, 64 | vtoclgaf 3271 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
66 | 65 | impcom 446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
67 | 66 | pm5.32da 673 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
68 | 30, 67 | bitrd 268 |
. . . . 5
⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
69 | 19, 68 | syl5bb 272 |
. . . 4
⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
70 | 14, 69 | bitrd 268 |
. . 3
⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
71 | | vex 3203 |
. . . 4
⊢ 𝑧 ∈ V |
72 | 71, 47 | opelco 5293 |
. . 3
⊢
(〈𝑧, 𝑤〉 ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) |
73 | | df-mpt 4730 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {〈𝑥, 𝑣〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} |
74 | 73 | eleq2i 2693 |
. . . 4
⊢
(〈𝑧, 𝑤〉 ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑣〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}) |
75 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
76 | 37 | nfeq2 2780 |
. . . . . 6
⊢
Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇 |
77 | 75, 76 | nfan 1828 |
. . . . 5
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) |
78 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇) |
79 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
80 | 43 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)) |
81 | 79, 80 | anbi12d 747 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))) |
82 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
83 | 82 | anbi2d 740 |
. . . . 5
⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
84 | 77, 78, 71, 47, 81, 83 | opelopabf 5000 |
. . . 4
⊢
(〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑣〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
85 | 74, 84 | bitri 264 |
. . 3
⊢
(〈𝑧, 𝑤〉 ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
86 | 70, 72, 85 | 3bitr4g 303 |
. 2
⊢ (𝜑 → (〈𝑧, 𝑤〉 ∈ (𝐺 ∘ 𝐹) ↔ 〈𝑧, 𝑤〉 ∈ (𝑥 ∈ 𝐴 ↦ 𝑇))) |
87 | 1, 2, 86 | eqrelrdv 5216 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |