Proof of Theorem pr2ne
Step | Hyp | Ref
| Expression |
1 | | preq2 4625 |
. . . . 5
⊢ (𝐵 = 𝐴 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
2 | 1 | eqcoms 2746 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
3 | | enpr1g 8622 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐶 → {𝐴, 𝐴} ≈ 1o) |
4 | | entr 8607 |
. . . . . . . . . . . 12
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1o) → {𝐴, 𝐵} ≈ 1o) |
5 | | 1sdom2 8796 |
. . . . . . . . . . . . . . 15
⊢
1o ≺ 2o |
6 | | sdomnen 8584 |
. . . . . . . . . . . . . . 15
⊢
(1o ≺ 2o → ¬ 1o ≈
2o) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ¬
1o ≈ 2o |
8 | | ensym 8604 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴, 𝐵} ≈ 1o → 1o
≈ {𝐴, 𝐵}) |
9 | | entr 8607 |
. . . . . . . . . . . . . . . 16
⊢
((1o ≈ {𝐴, 𝐵} ∧ {𝐴, 𝐵} ≈ 2o) →
1o ≈ 2o) |
10 | 9 | ex 416 |
. . . . . . . . . . . . . . 15
⊢
(1o ≈ {𝐴, 𝐵} → ({𝐴, 𝐵} ≈ 2o → 1o
≈ 2o)) |
11 | 8, 10 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ({𝐴, 𝐵} ≈ 1o → ({𝐴, 𝐵} ≈ 2o → 1o
≈ 2o)) |
12 | 7, 11 | mtoi 202 |
. . . . . . . . . . . . 13
⊢ ({𝐴, 𝐵} ≈ 1o → ¬ {𝐴, 𝐵} ≈ 2o) |
13 | 12 | a1d 25 |
. . . . . . . . . . . 12
⊢ ({𝐴, 𝐵} ≈ 1o → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o)) |
14 | 4, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (({𝐴, 𝐵} ≈ {𝐴, 𝐴} ∧ {𝐴, 𝐴} ≈ 1o) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o)) |
15 | 14 | ex 416 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} ≈ {𝐴, 𝐴} → ({𝐴, 𝐴} ≈ 1o → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o))) |
16 | | prex 5299 |
. . . . . . . . . . 11
⊢ {𝐴, 𝐵} ∈ V |
17 | | eqeng 8589 |
. . . . . . . . . . 11
⊢ ({𝐴, 𝐵} ∈ V → ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴})) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝐴, 𝐵} = {𝐴, 𝐴} → {𝐴, 𝐵} ≈ {𝐴, 𝐴}) |
19 | 15, 18 | syl11 33 |
. . . . . . . . 9
⊢ ({𝐴, 𝐴} ≈ 1o → ({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o))) |
20 | 19 | a1dd 50 |
. . . . . . . 8
⊢ ({𝐴, 𝐴} ≈ 1o → ({𝐴, 𝐵} = {𝐴, 𝐴} → (𝐵 ∈ 𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o)))) |
21 | 3, 20 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → ({𝐴, 𝐵} = {𝐴, 𝐴} → (𝐵 ∈ 𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o)))) |
22 | 21 | com23 86 |
. . . . . 6
⊢ (𝐴 ∈ 𝐶 → (𝐵 ∈ 𝐷 → ({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o)))) |
23 | 22 | imp 410 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ¬ {𝐴, 𝐵} ≈ 2o))) |
24 | 23 | pm2.43a 54 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} = {𝐴, 𝐴} → ¬ {𝐴, 𝐵} ≈ 2o)) |
25 | 2, 24 | syl5 34 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → ¬ {𝐴, 𝐵} ≈ 2o)) |
26 | 25 | necon2ad 2949 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o → 𝐴 ≠ 𝐵)) |
27 | | pr2nelem 9504 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o) |
28 | 27 | 3expia 1122 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} ≈ 2o)) |
29 | 26, 28 | impbid 215 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵)) |