Proof of Theorem pr2ne
Step | Hyp | Ref
| Expression |
1 | | preq2 4213 |
. . . . 5
⊢ (𝐵 = 𝐴 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
2 | 1 | eqcoms 2618 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
3 | | enpr1g 7908 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐶 → {𝐴, 𝐴} ≈
1𝑜) |
4 | | prex 4836 |
. . . . . . . . . . . 12
⊢ {𝐴, 𝐵} ∈ V |
5 | | eqeng 7875 |
. . . . . . . . . . . 12
⊢ ({𝐴, 𝐵} ∈ V → ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴})) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴}) |
7 | | entr 7894 |
. . . . . . . . . . . . 13
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1𝑜) →
{𝐴, 𝐵} ≈
1𝑜) |
8 | | 1sdom2 8044 |
. . . . . . . . . . . . . . . 16
⊢
1𝑜 ≺ 2𝑜 |
9 | | sdomnen 7870 |
. . . . . . . . . . . . . . . 16
⊢
(1𝑜 ≺ 2𝑜 → ¬
1𝑜 ≈ 2𝑜) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ¬
1𝑜 ≈ 2𝑜 |
11 | | ensym 7891 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
1𝑜 ≈ {𝐴, 𝐵}) |
12 | | entr 7894 |
. . . . . . . . . . . . . . . . 17
⊢
((1𝑜 ≈ {𝐴, 𝐵} ∧ {𝐴, 𝐵} ≈ 2𝑜) →
1𝑜 ≈ 2𝑜) |
13 | 12 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢
(1𝑜 ≈ {𝐴, 𝐵} → ({𝐴, 𝐵} ≈ 2𝑜 →
1𝑜 ≈ 2𝑜)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
({𝐴, 𝐵} ≈ 2𝑜 →
1𝑜 ≈ 2𝑜)) |
15 | 10, 14 | mtoi 189 |
. . . . . . . . . . . . . 14
⊢ ({𝐴, 𝐵} ≈ 1𝑜 → ¬
{𝐴, 𝐵} ≈
2𝑜) |
16 | 15 | a1d 25 |
. . . . . . . . . . . . 13
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
17 | 7, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1𝑜) →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
18 | 17 | ex 449 |
. . . . . . . . . . 11
⊢ ({𝐴, 𝐵} ≈ {𝐴, 𝐴} → ({𝐴, 𝐴} ≈ 1𝑜 →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
19 | 6, 18 | syl 17 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} = {𝐴, 𝐴} → ({𝐴, 𝐴} ≈ 1𝑜 →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
20 | 19 | com12 32 |
. . . . . . . . 9
⊢ ({𝐴, 𝐴} ≈ 1𝑜 →
({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
21 | 20 | a1dd 48 |
. . . . . . . 8
⊢ ({𝐴, 𝐴} ≈ 1𝑜 →
({𝐴, 𝐵} = {𝐴, 𝐴} → (𝐵 ∈ 𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)))) |
22 | 3, 21 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → ({𝐴, 𝐵} = {𝐴, 𝐴} → (𝐵 ∈ 𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)))) |
23 | 22 | com23 84 |
. . . . . 6
⊢ (𝐴 ∈ 𝐶 → (𝐵 ∈ 𝐷 → ({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)))) |
24 | 23 | imp 444 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
25 | 24 | pm2.43a 52 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
26 | 2, 25 | syl5 33 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
27 | 26 | necon2ad 2797 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2𝑜 → 𝐴 ≠ 𝐵)) |
28 | | pr2nelem 8710 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈
2𝑜) |
29 | 28 | 3expia 1259 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} ≈
2𝑜)) |
30 | 27, 29 | impbid 201 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2𝑜 ↔ 𝐴 ≠ 𝐵)) |