Step | Hyp | Ref
| Expression |
1 | | dfpss2 4049 |
. . . . . . . 8
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
2 | | php3 9162 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊊ 𝐵) → 𝐴 ≺ 𝐵) |
3 | | sdomnen 8927 |
. . . . . . . . . 10
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊊ 𝐵) → ¬ 𝐴 ≈ 𝐵) |
5 | 4 | ex 414 |
. . . . . . . 8
⊢ (𝐵 ∈ Fin → (𝐴 ⊊ 𝐵 → ¬ 𝐴 ≈ 𝐵)) |
6 | 1, 5 | biimtrrid 242 |
. . . . . . 7
⊢ (𝐵 ∈ Fin → ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 ≈ 𝐵)) |
7 | 6 | adantl 483 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 ≈ 𝐵)) |
8 | 7 | expd 417 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → ¬ 𝐴 ≈ 𝐵))) |
9 | | dfpss2 4049 |
. . . . . . . . 9
⊢ (𝐵 ⊊ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ ¬ 𝐵 = 𝐴)) |
10 | | eqcom 2740 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
11 | 10 | notbii 320 |
. . . . . . . . . 10
⊢ (¬
𝐵 = 𝐴 ↔ ¬ 𝐴 = 𝐵) |
12 | 11 | anbi2i 624 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ 𝐴 ∧ ¬ 𝐵 = 𝐴) ↔ (𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵)) |
13 | 9, 12 | bitri 275 |
. . . . . . . 8
⊢ (𝐵 ⊊ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵)) |
14 | | php3 9162 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) |
15 | | sdomnen 8927 |
. . . . . . . . . . 11
⊢ (𝐵 ≺ 𝐴 → ¬ 𝐵 ≈ 𝐴) |
16 | | ensym 8949 |
. . . . . . . . . . 11
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
17 | 15, 16 | nsyl 140 |
. . . . . . . . . 10
⊢ (𝐵 ≺ 𝐴 → ¬ 𝐴 ≈ 𝐵) |
18 | 14, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) |
19 | 18 | ex 414 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
20 | 13, 19 | biimtrrid 242 |
. . . . . . 7
⊢ (𝐴 ∈ Fin → ((𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 ≈ 𝐵)) |
21 | 20 | adantr 482 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 ≈ 𝐵)) |
22 | 21 | expd 417 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐵 ⊆ 𝐴 → (¬ 𝐴 = 𝐵 → ¬ 𝐴 ≈ 𝐵))) |
23 | 8, 22 | jaod 858 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) → (¬ 𝐴 = 𝐵 → ¬ 𝐴 ≈ 𝐵))) |
24 | 23 | 3impia 1118 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (¬ 𝐴 = 𝐵 → ¬ 𝐴 ≈ 𝐵)) |
25 | 24 | con4d 115 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵)) |
26 | | eqeng 8932 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
27 | 26 | 3ad2ant1 1134 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
28 | 25, 27 | impbid 211 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |