Proof of Theorem pr2ne
Step | Hyp | Ref
| Expression |
1 | | preq2 3470 |
. . . . 5
⊢ (𝐵 = 𝐴 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
2 | 1 | eqcoms 2084 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
3 | | enpr1g 6301 |
. . . . . 6
⊢ (𝐴 ∈ 𝐶 → {𝐴, 𝐴} ≈
1𝑜) |
4 | 3 | adantr 270 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐴} ≈
1𝑜) |
5 | | prexg 3966 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ∈ V) |
6 | | eqeng 6269 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∈ V → ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴})) |
7 | 5, 6 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴})) |
8 | | entr 6287 |
. . . . . . . . 9
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1𝑜) →
{𝐴, 𝐵} ≈
1𝑜) |
9 | | 1nen2 6347 |
. . . . . . . . . . 11
⊢ ¬
1𝑜 ≈ 2𝑜 |
10 | | ensym 6284 |
. . . . . . . . . . . 12
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
1𝑜 ≈ {𝐴, 𝐵}) |
11 | | entr 6287 |
. . . . . . . . . . . . 13
⊢
((1𝑜 ≈ {𝐴, 𝐵} ∧ {𝐴, 𝐵} ≈ 2𝑜) →
1𝑜 ≈ 2𝑜) |
12 | 11 | ex 113 |
. . . . . . . . . . . 12
⊢
(1𝑜 ≈ {𝐴, 𝐵} → ({𝐴, 𝐵} ≈ 2𝑜 →
1𝑜 ≈ 2𝑜)) |
13 | 10, 12 | syl 14 |
. . . . . . . . . . 11
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
({𝐴, 𝐵} ≈ 2𝑜 →
1𝑜 ≈ 2𝑜)) |
14 | 9, 13 | mtoi 622 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} ≈ 1𝑜 → ¬
{𝐴, 𝐵} ≈
2𝑜) |
15 | 14 | a1d 22 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
16 | 8, 15 | syl 14 |
. . . . . . . 8
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1𝑜) →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
17 | 16 | ex 113 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ≈ {𝐴, 𝐴} → ({𝐴, 𝐴} ≈ 1𝑜 →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
18 | 17 | com3r 78 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ {𝐴, 𝐴} → ({𝐴, 𝐴} ≈ 1𝑜 → ¬
{𝐴, 𝐵} ≈
2𝑜))) |
19 | 7, 18 | syld 44 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ({𝐴, 𝐴} ≈ 1𝑜 → ¬
{𝐴, 𝐵} ≈
2𝑜))) |
20 | 4, 19 | mpid 41 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
21 | 2, 20 | syl5 32 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
22 | 21 | necon2ad 2302 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2𝑜 → 𝐴 ≠ 𝐵)) |
23 | | pr2nelem 6460 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈
2𝑜) |
24 | 23 | 3expia 1140 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} ≈
2𝑜)) |
25 | 22, 24 | impbid 127 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2𝑜 ↔ 𝐴 ≠ 𝐵)) |