Step | Hyp | Ref
| Expression |
1 | | po0 5520 |
. . . . . 6
⊢ 𝑅 Po ∅ |
2 | | snprc 4653 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
3 | | poeq2 5507 |
. . . . . . 7
⊢ ({𝐴} = ∅ → (𝑅 Po {𝐴} ↔ 𝑅 Po ∅)) |
4 | 2, 3 | sylbi 216 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (𝑅 Po {𝐴} ↔ 𝑅 Po ∅)) |
5 | 1, 4 | mpbiri 257 |
. . . . 5
⊢ (¬
𝐴 ∈ V → 𝑅 Po {𝐴}) |
6 | 5 | adantl 482 |
. . . 4
⊢ ((Rel
𝑅 ∧ ¬ 𝐴 ∈ V) → 𝑅 Po {𝐴}) |
7 | | brrelex1 5640 |
. . . . 5
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐴) → 𝐴 ∈ V) |
8 | 7 | stoic1a 1775 |
. . . 4
⊢ ((Rel
𝑅 ∧ ¬ 𝐴 ∈ V) → ¬ 𝐴𝑅𝐴) |
9 | 6, 8 | 2thd 264 |
. . 3
⊢ ((Rel
𝑅 ∧ ¬ 𝐴 ∈ V) → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |
10 | 9 | ex 413 |
. 2
⊢ (Rel
𝑅 → (¬ 𝐴 ∈ V → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴))) |
11 | | df-po 5503 |
. . 3
⊢ (𝑅 Po {𝐴} ↔ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
12 | | breq2 5078 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → (𝑦𝑅𝑧 ↔ 𝑦𝑅𝐴)) |
13 | 12 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ↔ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴))) |
14 | | breq2 5078 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → (𝑥𝑅𝑧 ↔ 𝑥𝑅𝐴)) |
15 | 13, 14 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴))) |
16 | 15 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → ((¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
17 | 16 | ralsng 4609 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
18 | 17 | ralbidv 3112 |
. . . . . 6
⊢ (𝐴 ∈ V → (∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
19 | | simpl 483 |
. . . . . . . . . 10
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝑦) |
20 | | breq2 5078 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝐴)) |
21 | 19, 20 | syl5ib 243 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)) |
22 | 21 | biantrud 532 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (¬ 𝑥𝑅𝑥 ↔ (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
23 | 22 | bicomd 222 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ((¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)) ↔ ¬ 𝑥𝑅𝑥)) |
24 | 23 | ralsng 4609 |
. . . . . 6
⊢ (𝐴 ∈ V → (∀𝑦 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)) ↔ ¬ 𝑥𝑅𝑥)) |
25 | 18, 24 | bitrd 278 |
. . . . 5
⊢ (𝐴 ∈ V → (∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ¬ 𝑥𝑅𝑥)) |
26 | 25 | ralbidv 3112 |
. . . 4
⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ {𝐴} ¬ 𝑥𝑅𝑥)) |
27 | | breq12 5079 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑥𝑅𝑥 ↔ 𝐴𝑅𝐴)) |
28 | 27 | anidms 567 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥𝑅𝑥 ↔ 𝐴𝑅𝐴)) |
29 | 28 | notbid 318 |
. . . . 5
⊢ (𝑥 = 𝐴 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝐴𝑅𝐴)) |
30 | 29 | ralsng 4609 |
. . . 4
⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴} ¬ 𝑥𝑅𝑥 ↔ ¬ 𝐴𝑅𝐴)) |
31 | 26, 30 | bitrd 278 |
. . 3
⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ¬ 𝐴𝑅𝐴)) |
32 | 11, 31 | bitrid 282 |
. 2
⊢ (𝐴 ∈ V → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |
33 | 10, 32 | pm2.61d2 181 |
1
⊢ (Rel
𝑅 → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |