Step | Hyp | Ref
| Expression |
1 | | po0 5469 |
. . . . . 6
⊢ 𝑅 Po ∅ |
2 | | snprc 4618 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
3 | | poeq2 5456 |
. . . . . . 7
⊢ ({𝐴} = ∅ → (𝑅 Po {𝐴} ↔ 𝑅 Po ∅)) |
4 | 2, 3 | sylbi 220 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (𝑅 Po {𝐴} ↔ 𝑅 Po ∅)) |
5 | 1, 4 | mpbiri 261 |
. . . . 5
⊢ (¬
𝐴 ∈ V → 𝑅 Po {𝐴}) |
6 | 5 | adantl 485 |
. . . 4
⊢ ((Rel
𝑅 ∧ ¬ 𝐴 ∈ V) → 𝑅 Po {𝐴}) |
7 | | brrelex1 5586 |
. . . . 5
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐴) → 𝐴 ∈ V) |
8 | 7 | stoic1a 1779 |
. . . 4
⊢ ((Rel
𝑅 ∧ ¬ 𝐴 ∈ V) → ¬ 𝐴𝑅𝐴) |
9 | 6, 8 | 2thd 268 |
. . 3
⊢ ((Rel
𝑅 ∧ ¬ 𝐴 ∈ V) → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |
10 | 9 | ex 416 |
. 2
⊢ (Rel
𝑅 → (¬ 𝐴 ∈ V → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴))) |
11 | | df-po 5452 |
. . 3
⊢ (𝑅 Po {𝐴} ↔ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
12 | | breq2 5044 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → (𝑦𝑅𝑧 ↔ 𝑦𝑅𝐴)) |
13 | 12 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ↔ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴))) |
14 | | breq2 5044 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → (𝑥𝑅𝑧 ↔ 𝑥𝑅𝐴)) |
15 | 13, 14 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴))) |
16 | 15 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → ((¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
17 | 16 | ralsng 4574 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
18 | 17 | ralbidv 3110 |
. . . . . 6
⊢ (𝐴 ∈ V → (∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
19 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝑦) |
20 | | breq2 5044 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝐴)) |
21 | 19, 20 | syl5ib 247 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)) |
22 | 21 | biantrud 535 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (¬ 𝑥𝑅𝑥 ↔ (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)))) |
23 | 22 | bicomd 226 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ((¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)) ↔ ¬ 𝑥𝑅𝑥)) |
24 | 23 | ralsng 4574 |
. . . . . 6
⊢ (𝐴 ∈ V → (∀𝑦 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐴) → 𝑥𝑅𝐴)) ↔ ¬ 𝑥𝑅𝑥)) |
25 | 18, 24 | bitrd 282 |
. . . . 5
⊢ (𝐴 ∈ V → (∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ¬ 𝑥𝑅𝑥)) |
26 | 25 | ralbidv 3110 |
. . . 4
⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ {𝐴} ¬ 𝑥𝑅𝑥)) |
27 | | breq12 5045 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑥𝑅𝑥 ↔ 𝐴𝑅𝐴)) |
28 | 27 | anidms 570 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥𝑅𝑥 ↔ 𝐴𝑅𝐴)) |
29 | 28 | notbid 321 |
. . . . 5
⊢ (𝑥 = 𝐴 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝐴𝑅𝐴)) |
30 | 29 | ralsng 4574 |
. . . 4
⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴} ¬ 𝑥𝑅𝑥 ↔ ¬ 𝐴𝑅𝐴)) |
31 | 26, 30 | bitrd 282 |
. . 3
⊢ (𝐴 ∈ V → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴}∀𝑧 ∈ {𝐴} (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ¬ 𝐴𝑅𝐴)) |
32 | 11, 31 | syl5bb 286 |
. 2
⊢ (𝐴 ∈ V → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |
33 | 10, 32 | pm2.61d2 184 |
1
⊢ (Rel
𝑅 → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |