Proof of Theorem pr2ne
Step | Hyp | Ref
| Expression |
1 | | preq2 4413 |
. . . . 5
⊢ (𝐵 = 𝐴 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
2 | 1 | eqcoms 2768 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
3 | | enpr1g 8189 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐶 → {𝐴, 𝐴} ≈
1𝑜) |
4 | | entr 8175 |
. . . . . . . . . . . 12
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1𝑜) →
{𝐴, 𝐵} ≈
1𝑜) |
5 | | 1sdom2 8326 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ≺ 2𝑜 |
6 | | sdomnen 8152 |
. . . . . . . . . . . . . . 15
⊢
(1𝑜 ≺ 2𝑜 → ¬
1𝑜 ≈ 2𝑜) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ¬
1𝑜 ≈ 2𝑜 |
8 | | ensym 8172 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
1𝑜 ≈ {𝐴, 𝐵}) |
9 | | entr 8175 |
. . . . . . . . . . . . . . . 16
⊢
((1𝑜 ≈ {𝐴, 𝐵} ∧ {𝐴, 𝐵} ≈ 2𝑜) →
1𝑜 ≈ 2𝑜) |
10 | 9 | ex 449 |
. . . . . . . . . . . . . . 15
⊢
(1𝑜 ≈ {𝐴, 𝐵} → ({𝐴, 𝐵} ≈ 2𝑜 →
1𝑜 ≈ 2𝑜)) |
11 | 8, 10 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
({𝐴, 𝐵} ≈ 2𝑜 →
1𝑜 ≈ 2𝑜)) |
12 | 7, 11 | mtoi 190 |
. . . . . . . . . . . . 13
⊢ ({𝐴, 𝐵} ≈ 1𝑜 → ¬
{𝐴, 𝐵} ≈
2𝑜) |
13 | 12 | a1d 25 |
. . . . . . . . . . . 12
⊢ ({𝐴, 𝐵} ≈ 1𝑜 →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
14 | 4, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1𝑜) →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
15 | 14 | ex 449 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} ≈ {𝐴, 𝐴} → ({𝐴, 𝐴} ≈ 1𝑜 →
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
16 | | prex 5058 |
. . . . . . . . . . 11
⊢ {𝐴, 𝐵} ∈ V |
17 | | eqeng 8157 |
. . . . . . . . . . 11
⊢ ({𝐴, 𝐵} ∈ V → ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴})) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴}) |
19 | 15, 18 | syl11 33 |
. . . . . . . . 9
⊢ ({𝐴, 𝐴} ≈ 1𝑜 →
({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
20 | 19 | a1dd 50 |
. . . . . . . 8
⊢ ({𝐴, 𝐴} ≈ 1𝑜 →
({𝐴, 𝐵} = {𝐴, 𝐴} → (𝐵 ∈ 𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)))) |
21 | 3, 20 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → ({𝐴, 𝐵} = {𝐴, 𝐴} → (𝐵 ∈ 𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)))) |
22 | 21 | com23 86 |
. . . . . 6
⊢ (𝐴 ∈ 𝐶 → (𝐵 ∈ 𝐷 → ({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜)))) |
23 | 22 | imp 444 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈
2𝑜))) |
24 | 23 | pm2.43a 54 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
25 | 2, 24 | syl5 34 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → ¬ {𝐴, 𝐵} ≈
2𝑜)) |
26 | 25 | necon2ad 2947 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2𝑜 → 𝐴 ≠ 𝐵)) |
27 | | pr2nelem 9037 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈
2𝑜) |
28 | 27 | 3expia 1115 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} ≈
2𝑜)) |
29 | 26, 28 | impbid 202 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2𝑜 ↔ 𝐴 ≠ 𝐵)) |