Proof of Theorem dmrelrnrel
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
⊢ (𝜑 → 𝜑) |
2 | | dmrelrnrel.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
3 | | dmrelrnrel.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
4 | 1, 2, 3 | jca31 518 |
. 2
⊢ (𝜑 → ((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴)) |
5 | | dmrelrnrel.r |
. 2
⊢ (𝜑 → 𝐵𝑅𝐶) |
6 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑦 𝐵 ∈ 𝐴 |
7 | | dmrelrnrel.y |
. . . . . . . 8
⊢
Ⅎ𝑦𝜑 |
8 | 7, 6 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜑 ∧ 𝐵 ∈ 𝐴) |
9 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑦 𝐶 ∈ 𝐴 |
10 | 8, 9 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑦((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴) |
11 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑦(𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)) |
12 | 10, 11 | nfim 1903 |
. . . . 5
⊢
Ⅎ𝑦(((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶))) |
13 | 6, 12 | nfim 1903 |
. . . 4
⊢
Ⅎ𝑦(𝐵 ∈ 𝐴 → (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)))) |
14 | | eleq1 2820 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
15 | 14 | anbi2d 632 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ↔ ((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴))) |
16 | | breq2 5034 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (𝐵𝑅𝑦 ↔ 𝐵𝑅𝐶)) |
17 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → (𝐹‘𝑦) = (𝐹‘𝐶)) |
18 | 17 | breq2d 5042 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → ((𝐹‘𝐵)𝑆(𝐹‘𝑦) ↔ (𝐹‘𝐵)𝑆(𝐹‘𝐶))) |
19 | 16, 18 | imbi12d 348 |
. . . . . 6
⊢ (𝑦 = 𝐶 → ((𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦)) ↔ (𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)))) |
20 | 15, 19 | imbi12d 348 |
. . . . 5
⊢ (𝑦 = 𝐶 → ((((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦))) ↔ (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶))))) |
21 | 20 | imbi2d 344 |
. . . 4
⊢ (𝑦 = 𝐶 → ((𝐵 ∈ 𝐴 → (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦)))) ↔ (𝐵 ∈ 𝐴 → (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)))))) |
22 | | dmrelrnrel.x |
. . . . . . . 8
⊢
Ⅎ𝑥𝜑 |
23 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝐵 ∈ 𝐴 |
24 | 22, 23 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝐵 ∈ 𝐴) |
25 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
26 | 24, 25 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑥((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) |
27 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑥(𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦)) |
28 | 26, 27 | nfim 1903 |
. . . . 5
⊢
Ⅎ𝑥(((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦))) |
29 | | eleq1 2820 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
30 | 29 | anbi2d 632 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝐵 ∈ 𝐴))) |
31 | 30 | anbi1d 633 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ↔ ((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴))) |
32 | | breq1 5033 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥𝑅𝑦 ↔ 𝐵𝑅𝑦)) |
33 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
34 | 33 | breq1d 5040 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥)𝑆(𝐹‘𝑦) ↔ (𝐹‘𝐵)𝑆(𝐹‘𝑦))) |
35 | 32, 34 | imbi12d 348 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦)) ↔ (𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦)))) |
36 | 31, 35 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) ↔ (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦))))) |
37 | | dmrelrnrel.i |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) |
38 | 37 | r19.21bi 3121 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) |
39 | 38 | r19.21bi 3121 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) |
40 | 28, 36, 39 | vtoclg1f 3469 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝐵𝑅𝑦 → (𝐹‘𝐵)𝑆(𝐹‘𝑦)))) |
41 | 13, 21, 40 | vtoclg1f 3469 |
. . 3
⊢ (𝐶 ∈ 𝐴 → (𝐵 ∈ 𝐴 → (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶))))) |
42 | 3, 2, 41 | sylc 65 |
. 2
⊢ (𝜑 → (((𝜑 ∧ 𝐵 ∈ 𝐴) ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)))) |
43 | 4, 5, 42 | mp2d 49 |
1
⊢ (𝜑 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)) |