Step | Hyp | Ref
| Expression |
1 | | simpll 481 |
. . . . . . . 8
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
x ∈
A) |
2 | | brinxp 4351 |
. . . . . . . 8
⊢
((x ∈ A ∧ x ∈ A) →
(x𝑅x ↔
x(𝑅 ∩ (A × A))x)) |
3 | 1, 1, 2 | syl2anc 391 |
. . . . . . 7
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
(x𝑅x ↔
x(𝑅 ∩ (A × A))x)) |
4 | 3 | notbid 591 |
. . . . . 6
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
(¬ x𝑅x ↔
¬ x(𝑅 ∩ (A × A))x)) |
5 | | brinxp 4351 |
. . . . . . . . 9
⊢
((x ∈ A ∧ y ∈ A) →
(x𝑅y ↔
x(𝑅 ∩ (A × A))y)) |
6 | 5 | adantr 261 |
. . . . . . . 8
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
(x𝑅y ↔
x(𝑅 ∩ (A × A))y)) |
7 | | brinxp 4351 |
. . . . . . . . 9
⊢
((y ∈ A ∧ z ∈ A) →
(y𝑅z ↔
y(𝑅 ∩ (A × A))z)) |
8 | 7 | adantll 445 |
. . . . . . . 8
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
(y𝑅z ↔
y(𝑅 ∩ (A × A))z)) |
9 | 6, 8 | anbi12d 442 |
. . . . . . 7
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
((x𝑅y ∧ y𝑅z) ↔ (x(𝑅 ∩ (A × A))y ∧ y(𝑅 ∩ (A × A))z))) |
10 | | brinxp 4351 |
. . . . . . . 8
⊢
((x ∈ A ∧ z ∈ A) →
(x𝑅z ↔
x(𝑅 ∩ (A × A))z)) |
11 | 10 | adantlr 446 |
. . . . . . 7
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
(x𝑅z ↔
x(𝑅 ∩ (A × A))z)) |
12 | 9, 11 | imbi12d 223 |
. . . . . 6
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
(((x𝑅y ∧ y𝑅z) → x𝑅z) ↔ ((x(𝑅 ∩ (A × A))y ∧ y(𝑅 ∩ (A × A))z) →
x(𝑅 ∩ (A × A))z))) |
13 | 4, 12 | anbi12d 442 |
. . . . 5
⊢
(((x ∈ A ∧ y ∈ A) ∧ z ∈ A) →
((¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z))
↔ (¬ x(𝑅 ∩ (A × A))x ∧ ((x(𝑅 ∩ (A × A))y ∧ y(𝑅 ∩ (A × A))z) →
x(𝑅 ∩ (A × A))z)))) |
14 | 13 | ralbidva 2316 |
. . . 4
⊢
((x ∈ A ∧ y ∈ A) →
(∀z
∈ A
(¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z))
↔ ∀z ∈ A (¬ x(𝑅 ∩ (A × A))x ∧ ((x(𝑅 ∩ (A × A))y ∧ y(𝑅 ∩ (A × A))z) →
x(𝑅 ∩ (A × A))z)))) |
15 | 14 | ralbidva 2316 |
. . 3
⊢ (x ∈ A → (∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z))
↔ ∀y ∈ A ∀z ∈ A (¬ x(𝑅 ∩ (A × A))x ∧ ((x(𝑅 ∩ (A × A))y ∧ y(𝑅 ∩ (A × A))z) →
x(𝑅 ∩ (A × A))z)))) |
16 | 15 | ralbiia 2332 |
. 2
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z))
↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ x(𝑅 ∩ (A × A))x ∧ ((x(𝑅 ∩ (A × A))y ∧ y(𝑅 ∩ (A × A))z) →
x(𝑅 ∩ (A × A))z))) |
17 | | df-po 4024 |
. 2
⊢ (𝑅 Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z))) |
18 | | df-po 4024 |
. 2
⊢ ((𝑅 ∩ (A × A)) Po
A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬
x(𝑅 ∩ (A × A))x ∧ ((x(𝑅 ∩ (A × A))y ∧ y(𝑅 ∩ (A × A))z) →
x(𝑅 ∩ (A × A))z))) |
19 | 16, 17, 18 | 3bitr4i 201 |
1
⊢ (𝑅 Po A ↔ (𝑅 ∩ (A × A)) Po
A) |