Step | Hyp | Ref
| Expression |
1 | | elirr 4540 |
. . . . . 6
⊢ ¬
𝐴 ∈ 𝐴 |
2 | | eleq2 2241 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐴 ↔ 𝐴 ∈ 𝐵)) |
3 | 1, 2 | mtbii 674 |
. . . . 5
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ∈ 𝐵) |
4 | 3 | con2i 627 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 = 𝐵) |
5 | 4 | adantl 277 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ 𝐵) → ¬ 𝐴 = 𝐵) |
6 | | simpl 109 |
. . . . 5
⊢ ((¬
𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴) → ¬ 𝐴 ∈ 𝐵) |
7 | 6 | con2i 627 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ¬ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)) |
8 | 7 | adantl 277 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ 𝐵) → ¬ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)) |
9 | 5, 8 | 2falsed 702 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ 𝐵) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))) |
10 | | simpr 110 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
11 | | eleq1 2240 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
12 | 1, 11 | mtbii 674 |
. . . . 5
⊢ (𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴) |
13 | 3, 12 | jca 306 |
. . . 4
⊢ (𝐴 = 𝐵 → (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)) |
14 | 13 | adantl 277 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 = 𝐵) → (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)) |
15 | 10, 14 | 2thd 175 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 = 𝐵) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))) |
16 | 12 | con2i 627 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = 𝐵) |
17 | 16 | adantl 277 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ∈ 𝐴) → ¬ 𝐴 = 𝐵) |
18 | | simpr 110 |
. . . . 5
⊢ ((¬
𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ 𝐴) |
19 | 18 | con2i 627 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → ¬ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)) |
20 | 19 | adantl 277 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ∈ 𝐴) → ¬ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)) |
21 | 17, 20 | 2falsed 702 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ∈ 𝐴) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))) |
22 | | nntri3or 6493 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |
23 | 9, 15, 21, 22 | mpjao3dan 1307 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))) |