Proof of Theorem isso2i
Step | Hyp | Ref
| Expression |
1 | | equid 2015 |
. . . . 5
⊢ 𝑥 = 𝑥 |
2 | 1 | orci 862 |
. . . 4
⊢ (𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) |
3 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑦((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) ↔ ¬ 𝑥𝑅𝑥)) |
4 | | eleq1w 2821 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
5 | 4 | anbi2d 629 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴))) |
6 | | equequ2 2029 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑥)) |
7 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦𝑅𝑥 ↔ 𝑥𝑅𝑥)) |
8 | 6, 7 | orbi12d 916 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥 = 𝑥 ∨ 𝑥𝑅𝑥))) |
9 | | breq2 5078 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑥)) |
10 | 9 | notbid 318 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑥)) |
11 | 8, 10 | bibi12d 346 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ¬ 𝑥𝑅𝑦) ↔ ((𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) ↔ ¬ 𝑥𝑅𝑥))) |
12 | 5, 11 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ¬ 𝑥𝑅𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) ↔ ¬ 𝑥𝑅𝑥)))) |
13 | | isso2i.1 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
14 | 13 | con2bid 355 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ¬ 𝑥𝑅𝑦)) |
15 | 3, 12, 14 | chvarfv 2233 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑥 = 𝑥 ∨ 𝑥𝑅𝑥) ↔ ¬ 𝑥𝑅𝑥)) |
16 | 2, 15 | mpbii 232 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) |
17 | 16 | anidms 567 |
. 2
⊢ (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) |
18 | | isso2i.2 |
. 2
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
19 | 14 | biimprd 247 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (¬ 𝑥𝑅𝑦 → (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
20 | 19 | orrd 860 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
21 | | 3orass 1089 |
. . 3
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
22 | 20, 21 | sylibr 233 |
. 2
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
23 | 17, 18, 22 | issoi 5537 |
1
⊢ 𝑅 Or 𝐴 |