Step | Hyp | Ref
| Expression |
1 | | endom 8926 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
2 | | nnfi 9118 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → 𝐵 ∈ Fin) |
3 | | domfi 9143 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵) → 𝐴 ∈ Fin) |
4 | | simpr 486 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐵) |
5 | 3, 4 | jca 513 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵) → (𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵)) |
6 | | domnsymfi 9154 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ≺ 𝐴) |
7 | 6 | ex 414 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴)) |
8 | | php3 9163 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) |
9 | 8 | ex 414 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴)) |
10 | 7, 9 | nsyld 156 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin → (𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴)) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ Fin) → (𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴)) |
12 | 11 | expimpd 455 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ω → ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ⊊ 𝐴)) |
13 | 5, 12 | syl5 34 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ⊊ 𝐴)) |
14 | 2, 13 | mpand 694 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → (𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴)) |
15 | 14 | adantl 483 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴)) |
16 | | eloni 6332 |
. . . . . . . 8
⊢ (𝐴 ∈ On → Ord 𝐴) |
17 | | nnord 7815 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → Ord 𝐵) |
18 | | ordtri1 6355 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) |
19 | | ordelpss 6350 |
. . . . . . . . . . 11
⊢ ((Ord
𝐵 ∧ Ord 𝐴) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴)) |
20 | 19 | ancoms 460 |
. . . . . . . . . 10
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴)) |
21 | 20 | notbid 318 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ⊊ 𝐴)) |
22 | 18, 21 | bitrd 279 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ⊊ 𝐴)) |
23 | 16, 17, 22 | syl2an 597 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ⊊ 𝐴)) |
24 | 15, 23 | sylibrd 259 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 → 𝐴 ⊆ 𝐵)) |
25 | 1, 24 | syl5 34 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 → 𝐴 ⊆ 𝐵)) |
26 | 25 | 3impia 1118 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵) → 𝐴 ⊆ 𝐵) |
27 | | ensymfib 9138 |
. . . . . . . . 9
⊢ (𝐵 ∈ Fin → (𝐵 ≈ 𝐴 ↔ 𝐴 ≈ 𝐵)) |
28 | 2, 27 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → (𝐵 ≈ 𝐴 ↔ 𝐴 ≈ 𝐵)) |
29 | | endom 8926 |
. . . . . . . 8
⊢ (𝐵 ≈ 𝐴 → 𝐵 ≼ 𝐴) |
30 | 28, 29 | syl6bir 254 |
. . . . . . 7
⊢ (𝐵 ∈ ω → (𝐴 ≈ 𝐵 → 𝐵 ≼ 𝐴)) |
31 | 30 | imp 408 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵) → 𝐵 ≼ 𝐴) |
32 | 31 | 3adant1 1131 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵) → 𝐵 ≼ 𝐴) |
33 | | nndomog 9167 |
. . . . . . 7
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ≼ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
34 | 33 | ancoms 460 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐵 ≼ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
35 | 34 | biimp3a 1470 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐵 ≼ 𝐴) → 𝐵 ⊆ 𝐴) |
36 | 32, 35 | syld3an3 1410 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵) → 𝐵 ⊆ 𝐴) |
37 | 26, 36 | eqssd 3966 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) |
38 | 37 | 3expia 1122 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵)) |
39 | | enrefnn 8998 |
. . . 4
⊢ (𝐵 ∈ ω → 𝐵 ≈ 𝐵) |
40 | | breq1 5113 |
. . . 4
⊢ (𝐴 = 𝐵 → (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐵)) |
41 | 39, 40 | syl5ibrcom 247 |
. . 3
⊢ (𝐵 ∈ ω → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
42 | 41 | adantl 483 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
43 | 38, 42 | impbid 211 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |