Step | Hyp | Ref
| Expression |
1 | | trd.5 |
. 2
⊢ (φ → XRY) |
2 | | trd.6 |
. 2
⊢ (φ → YRZ) |
3 | | trd.1 |
. . . 4
⊢ (φ → R Trans A) |
4 | | brex 4690 |
. . . . . 6
⊢ (R Trans A → (R
∈ V ∧
A ∈
V)) |
5 | | breq 4642 |
. . . . . . . . . . 11
⊢ (r = R →
(xry ↔
xRy)) |
6 | | breq 4642 |
. . . . . . . . . . 11
⊢ (r = R →
(yrz ↔
yRz)) |
7 | 5, 6 | anbi12d 691 |
. . . . . . . . . 10
⊢ (r = R →
((xry ∧ yrz) ↔
(xRy ∧ yRz))) |
8 | | breq 4642 |
. . . . . . . . . 10
⊢ (r = R →
(xrz ↔
xRz)) |
9 | 7, 8 | imbi12d 311 |
. . . . . . . . 9
⊢ (r = R →
(((xry ∧ yrz) →
xrz) ↔
((xRy ∧ yRz) →
xRz))) |
10 | 9 | ralbidv 2635 |
. . . . . . . 8
⊢ (r = R →
(∀z
∈ a
((xry ∧ yrz) →
xrz) ↔ ∀z ∈ a ((xRy ∧ yRz) → xRz))) |
11 | 10 | 2ralbidv 2657 |
. . . . . . 7
⊢ (r = R →
(∀x
∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xRy ∧ yRz) → xRz))) |
12 | | raleq 2808 |
. . . . . . . . 9
⊢ (a = A →
(∀z
∈ a
((xRy ∧ yRz) →
xRz) ↔ ∀z ∈ A ((xRy ∧ yRz) → xRz))) |
13 | 12 | raleqbi1dv 2816 |
. . . . . . . 8
⊢ (a = A →
(∀y
∈ a ∀z ∈ a ((xRy ∧ yRz) → xRz) ↔ ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz))) |
14 | 13 | raleqbi1dv 2816 |
. . . . . . 7
⊢ (a = A →
(∀x
∈ a ∀y ∈ a ∀z ∈ a ((xRy ∧ yRz) → xRz) ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz))) |
15 | | df-trans 5900 |
. . . . . . 7
⊢ Trans = {〈r, a〉 ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)} |
16 | 11, 14, 15 | brabg 4707 |
. . . . . 6
⊢ ((R ∈ V ∧ A ∈ V) → (R
Trans A ↔
∀x
∈ A ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz))) |
17 | 4, 16 | syl 15 |
. . . . 5
⊢ (R Trans A → (R
Trans A ↔
∀x
∈ A ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz))) |
18 | 17 | ibi 232 |
. . . 4
⊢ (R Trans A → ∀x ∈ A ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz)) |
19 | 3, 18 | syl 15 |
. . 3
⊢ (φ → ∀x ∈ A ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz)) |
20 | | trd.2 |
. . . 4
⊢ (φ → X ∈ A) |
21 | | trd.3 |
. . . 4
⊢ (φ → Y ∈ A) |
22 | | trd.4 |
. . . 4
⊢ (φ → Z ∈ A) |
23 | | breq1 4643 |
. . . . . . 7
⊢ (x = X →
(xRy ↔
XRy)) |
24 | 23 | anbi1d 685 |
. . . . . 6
⊢ (x = X →
((xRy ∧ yRz) ↔
(XRy ∧ yRz))) |
25 | | breq1 4643 |
. . . . . 6
⊢ (x = X →
(xRz ↔
XRz)) |
26 | 24, 25 | imbi12d 311 |
. . . . 5
⊢ (x = X →
(((xRy ∧ yRz) →
xRz) ↔
((XRy ∧ yRz) →
XRz))) |
27 | | breq2 4644 |
. . . . . . 7
⊢ (y = Y →
(XRy ↔
XRY)) |
28 | | breq1 4643 |
. . . . . . 7
⊢ (y = Y →
(yRz ↔
YRz)) |
29 | 27, 28 | anbi12d 691 |
. . . . . 6
⊢ (y = Y →
((XRy ∧ yRz) ↔
(XRY ∧ YRz))) |
30 | 29 | imbi1d 308 |
. . . . 5
⊢ (y = Y →
(((XRy ∧ yRz) →
XRz) ↔
((XRY ∧ YRz) →
XRz))) |
31 | | breq2 4644 |
. . . . . . 7
⊢ (z = Z →
(YRz ↔
YRZ)) |
32 | 31 | anbi2d 684 |
. . . . . 6
⊢ (z = Z →
((XRY ∧ YRz) ↔
(XRY ∧ YRZ))) |
33 | | breq2 4644 |
. . . . . 6
⊢ (z = Z →
(XRz ↔
XRZ)) |
34 | 32, 33 | imbi12d 311 |
. . . . 5
⊢ (z = Z →
(((XRY ∧ YRz) →
XRz) ↔
((XRY ∧ YRZ) →
XRZ))) |
35 | 26, 30, 34 | rspc3v 2965 |
. . . 4
⊢ ((X ∈ A ∧ Y ∈ A ∧ Z ∈ A) → (∀x ∈ A ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz) → ((XRY ∧ YRZ) → XRZ))) |
36 | 20, 21, 22, 35 | syl3anc 1182 |
. . 3
⊢ (φ → (∀x ∈ A ∀y ∈ A ∀z ∈ A ((xRy ∧ yRz) → xRz) → ((XRY ∧ YRZ) → XRZ))) |
37 | 19, 36 | mpd 14 |
. 2
⊢ (φ → ((XRY ∧ YRZ) → XRZ)) |
38 | 1, 2, 37 | mp2and 660 |
1
⊢ (φ → XRZ) |