Step | Hyp | Ref
| Expression |
1 | | relco 5633 |
. 2
⊢ Rel
(𝐺 ∘ 𝐹) |
2 | | funmpt 5926 |
. . 3
⊢ Fun
(𝑥 ∈ 𝐴 ↦ 𝑇) |
3 | | funrel 5905 |
. . 3
⊢ (Fun
(𝑥 ∈ 𝐴 ↦ 𝑇) → Rel (𝑥 ∈ 𝐴 ↦ 𝑇)) |
4 | 2, 3 | ax-mp 5 |
. 2
⊢ Rel
(𝑥 ∈ 𝐴 ↦ 𝑇) |
5 | | fmptcof2.3 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝜑 |
6 | | fmptcof2.1 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐴 |
7 | | fmptcof2.2 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐵 |
8 | | fmptcof2.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) |
9 | 8 | r19.21bi 2932 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵) |
10 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
11 | 5, 6, 7, 9, 10 | fmptdF 29456 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶𝐵) |
12 | | fmptcof2.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) |
13 | 12 | feq1d 6030 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶𝐵)) |
14 | 11, 13 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
15 | | ffun 6048 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) |
17 | | funbrfv 6234 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢)) |
18 | 17 | imp 445 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢) |
19 | 16, 18 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢) |
20 | 19 | eqcomd 2628 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧)) |
21 | 20 | a1d 25 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧))) |
22 | 21 | expimpd 629 |
. . . . . 6
⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧))) |
23 | 22 | pm4.71rd 667 |
. . . . 5
⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)))) |
24 | 23 | exbidv 1850 |
. . . 4
⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)))) |
25 | | fvex 6201 |
. . . . . 6
⊢ (𝐹‘𝑧) ∈ V |
26 | | breq2 4657 |
. . . . . . 7
⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧))) |
27 | | breq1 4656 |
. . . . . . 7
⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤)) |
28 | 26, 27 | anbi12d 747 |
. . . . . 6
⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤))) |
29 | 25, 28 | ceqsexv 3242 |
. . . . 5
⊢
(∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)) |
30 | | funfvbrb 6330 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧))) |
31 | 16, 30 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧))) |
32 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
33 | 14, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
34 | 33 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴)) |
35 | 31, 34 | bitr3d 270 |
. . . . . . 7
⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴)) |
36 | 12 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)) |
37 | | fmptcof2.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) |
38 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → 𝑤 = 𝑤) |
39 | 36, 37, 38 | breq123d 4667 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)) |
40 | 35, 39 | anbi12d 747 |
. . . . . 6
⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))) |
41 | 6 | nfcri 2758 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
42 | | nffvmpt1 6199 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧) |
43 | | fmptcof2.x |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑆 |
44 | 7, 43 | nfmpt 4746 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆) |
45 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑤 |
46 | 42, 44, 45 | nfbr 4699 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 |
47 | | nfcsb1v 3549 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇 |
48 | 47 | nfeq2 2780 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇 |
49 | 46, 48 | nfbi 1833 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇) |
50 | 5, 49 | nfim 1825 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
51 | 41, 50 | nfim 1825 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
52 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
53 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)) |
54 | 53 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)) |
55 | | csbeq1a 3542 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇) |
56 | 55 | eqeq2d 2632 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
57 | 54, 56 | bibi12d 335 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
58 | 57 | imbi2d 330 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))) |
59 | 52, 58 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))) ↔ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))) |
60 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑤 ∈ V |
61 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝑅 ∈ 𝐵 |
62 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑤 |
63 | | fmptcof2.y |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑇 |
64 | 62, 63 | nfeq 2776 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝑤 = 𝑇 |
65 | 61, 64 | nfan 1828 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇) |
66 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅) |
67 | 66 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵)) |
68 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤) |
69 | | fmptcof2.7 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑆 = 𝑇) |
71 | 68, 70 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇)) |
72 | 67, 71 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
73 | | df-mpt 4730 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {〈𝑦, 𝑢〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)} |
74 | 65, 72, 73 | brabgaf 29420 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
75 | 9, 60, 74 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
76 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
77 | 6 | fvmpt2f 6283 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
78 | 76, 9, 77 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
79 | 78 | breq1d 4663 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)) |
80 | 9 | biantrurd 529 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇))) |
81 | 75, 79, 80 | 3bitr4d 300 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) |
82 | 81 | expcom 451 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))) |
83 | 51, 59, 82 | chvar 2262 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
84 | 83 | impcom 446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
85 | 84 | pm5.32da 673 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
86 | 40, 85 | bitrd 268 |
. . . . 5
⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
87 | 29, 86 | syl5bb 272 |
. . . 4
⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
88 | 24, 87 | bitrd 268 |
. . 3
⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
89 | | vex 3203 |
. . . 4
⊢ 𝑧 ∈ V |
90 | 89, 60 | opelco 5293 |
. . 3
⊢
(〈𝑧, 𝑤〉 ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) |
91 | | df-mpt 4730 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {〈𝑥, 𝑣〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} |
92 | 91 | eleq2i 2693 |
. . . 4
⊢
(〈𝑧, 𝑤〉 ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑣〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}) |
93 | 47 | nfeq2 2780 |
. . . . . 6
⊢
Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇 |
94 | 41, 93 | nfan 1828 |
. . . . 5
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) |
95 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇) |
96 | 55 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)) |
97 | 52, 96 | anbi12d 747 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))) |
98 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
99 | 98 | anbi2d 740 |
. . . . 5
⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))) |
100 | 94, 95, 89, 60, 97, 99 | opelopabf 5000 |
. . . 4
⊢
(〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑣〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
101 | 92, 100 | bitri 264 |
. . 3
⊢
(〈𝑧, 𝑤〉 ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) |
102 | 88, 90, 101 | 3bitr4g 303 |
. 2
⊢ (𝜑 → (〈𝑧, 𝑤〉 ∈ (𝐺 ∘ 𝐹) ↔ 〈𝑧, 𝑤〉 ∈ (𝑥 ∈ 𝐴 ↦ 𝑇))) |
103 | 1, 4, 102 | eqrelrdv 5216 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |