Proof of Theorem isso2i
Step | Hyp | Ref
| Expression |
1 | | equid 1926 |
. . . . 5
⊢ 𝑥 = 𝑥 |
2 | 1 | orci 404 |
. . . 4
⊢ (𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) |
3 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
4 | 3 | anbi2d 736 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴))) |
5 | | equequ2 1940 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑥)) |
6 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦𝑅𝑥 ↔ 𝑥𝑅𝑥)) |
7 | 5, 6 | orbi12d 742 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥 = 𝑥 ∨ 𝑥𝑅𝑥))) |
8 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑥)) |
9 | 8 | notbid 307 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑥)) |
10 | 7, 9 | bibi12d 334 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ¬ 𝑥𝑅𝑦) ↔ ((𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) ↔ ¬ 𝑥𝑅𝑥))) |
11 | 4, 10 | imbi12d 333 |
. . . . 5
⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ¬ 𝑥𝑅𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) ↔ ¬ 𝑥𝑅𝑥)))) |
12 | | isso2i.1 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
13 | 12 | con2bid 343 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ¬ 𝑥𝑅𝑦)) |
14 | 11, 13 | chvarv 2251 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) ↔ ¬ 𝑥𝑅𝑥)) |
15 | 2, 14 | mpbii 222 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) |
16 | 15 | anidms 675 |
. 2
⊢ (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) |
17 | | isso2i.2 |
. 2
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
18 | 13 | biimprd 237 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (¬ 𝑥𝑅𝑦 → (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
19 | 18 | orrd 392 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
20 | | 3orass 1034 |
. . 3
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
21 | 19, 20 | sylibr 223 |
. 2
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
22 | 16, 17, 21 | issoi 4990 |
1
⊢ 𝑅 Or 𝐴 |