Step | Hyp | Ref
| Expression |
1 | | df-po 4024 |
. 2
⊢ (𝑅 Po {A} ↔ ∀z ∈ {A}∀y ∈ {A}∀x ∈ {A} (¬
z𝑅z ∧ ((z𝑅y ∧ y𝑅x)
→ z𝑅x))) |
2 | | breq2 3759 |
. . . . . . . . . . 11
⊢ (x = A →
(y𝑅x ↔
y𝑅A)) |
3 | 2 | anbi2d 437 |
. . . . . . . . . 10
⊢ (x = A →
((z𝑅y ∧ y𝑅x) ↔ (z𝑅y ∧ y𝑅A))) |
4 | | breq2 3759 |
. . . . . . . . . 10
⊢ (x = A →
(z𝑅x ↔
z𝑅A)) |
5 | 3, 4 | imbi12d 223 |
. . . . . . . . 9
⊢ (x = A →
(((z𝑅y ∧ y𝑅x) → z𝑅x) ↔ ((z𝑅y ∧ y𝑅A) → z𝑅A))) |
6 | 5 | anbi2d 437 |
. . . . . . . 8
⊢ (x = A →
((¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅x)
→ z𝑅x))
↔ (¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅A)
→ z𝑅A)))) |
7 | 6 | ralsng 3402 |
. . . . . . 7
⊢ (A ∈ V →
(∀x
∈ {A}
(¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅x)
→ z𝑅x))
↔ (¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅A)
→ z𝑅A)))) |
8 | 7 | ralbidv 2320 |
. . . . . 6
⊢ (A ∈ V →
(∀y
∈ {A}∀x ∈ {A} (¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅x) → z𝑅x)) ↔ ∀y ∈ {A} (¬
z𝑅z ∧ ((z𝑅y ∧ y𝑅A)
→ z𝑅A)))) |
9 | | simpl 102 |
. . . . . . . . . 10
⊢
((z𝑅y ∧ y𝑅A) → z𝑅y) |
10 | | breq2 3759 |
. . . . . . . . . 10
⊢ (y = A →
(z𝑅y ↔
z𝑅A)) |
11 | 9, 10 | syl5ib 143 |
. . . . . . . . 9
⊢ (y = A →
((z𝑅y ∧ y𝑅A) → z𝑅A)) |
12 | 11 | biantrud 288 |
. . . . . . . 8
⊢ (y = A →
(¬ z𝑅z ↔
(¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅A)
→ z𝑅A)))) |
13 | 12 | bicomd 129 |
. . . . . . 7
⊢ (y = A →
((¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅A)
→ z𝑅A))
↔ ¬ z𝑅z)) |
14 | 13 | ralsng 3402 |
. . . . . 6
⊢ (A ∈ V →
(∀y
∈ {A}
(¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅A)
→ z𝑅A))
↔ ¬ z𝑅z)) |
15 | 8, 14 | bitrd 177 |
. . . . 5
⊢ (A ∈ V →
(∀y
∈ {A}∀x ∈ {A} (¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅x) → z𝑅x)) ↔ ¬ z𝑅z)) |
16 | 15 | ralbidv 2320 |
. . . 4
⊢ (A ∈ V →
(∀z
∈ {A}∀y ∈ {A}∀x ∈ {A} (¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅x) → z𝑅x)) ↔ ∀z ∈ {A} ¬
z𝑅z)) |
17 | | breq12 3760 |
. . . . . . 7
⊢
((z = A ∧ z = A) →
(z𝑅z ↔
A𝑅A)) |
18 | 17 | anidms 377 |
. . . . . 6
⊢ (z = A →
(z𝑅z ↔
A𝑅A)) |
19 | 18 | notbid 591 |
. . . . 5
⊢ (z = A →
(¬ z𝑅z ↔
¬ A𝑅A)) |
20 | 19 | ralsng 3402 |
. . . 4
⊢ (A ∈ V →
(∀z
∈ {A}
¬ z𝑅z ↔
¬ A𝑅A)) |
21 | 16, 20 | bitrd 177 |
. . 3
⊢ (A ∈ V →
(∀z
∈ {A}∀y ∈ {A}∀x ∈ {A} (¬ z𝑅z ∧ ((z𝑅y ∧ y𝑅x) → z𝑅x)) ↔ ¬ A𝑅A)) |
22 | 21 | adantl 262 |
. 2
⊢ ((Rel
𝑅 ∧ A ∈ V) → (∀z ∈ {A}∀y ∈ {A}∀x ∈ {A} (¬
z𝑅z ∧ ((z𝑅y ∧ y𝑅x)
→ z𝑅x))
↔ ¬ A𝑅A)) |
23 | 1, 22 | syl5bb 181 |
1
⊢ ((Rel
𝑅 ∧ A ∈ V) → (𝑅 Po {A}
↔ ¬ A𝑅A)) |