Step | Hyp | Ref
| Expression |
1 | | isfi 6721 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
2 | 1 | biimpi 119 |
. . 3
⊢ (𝐴 ∈ Fin → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
3 | 2 | ad2antrr 480 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
4 | | isfi 6721 |
. . . . 5
⊢ (𝐵 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐵 ≈ 𝑚) |
5 | 4 | biimpi 119 |
. . . 4
⊢ (𝐵 ∈ Fin → ∃𝑚 ∈ ω 𝐵 ≈ 𝑚) |
6 | 5 | ad3antlr 485 |
. . 3
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → ∃𝑚 ∈ ω 𝐵 ≈ 𝑚) |
7 | | simplrr 526 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝐴 ≈ 𝑛) |
8 | 7 | ensymd 6743 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑛 ≈ 𝐴) |
9 | | simprl 521 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≼ 𝐵) |
10 | 9 | ad2antrr 480 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝐴 ≼ 𝐵) |
11 | | endomtr 6750 |
. . . . . . . . 9
⊢ ((𝑛 ≈ 𝐴 ∧ 𝐴 ≼ 𝐵) → 𝑛 ≼ 𝐵) |
12 | 8, 10, 11 | syl2anc 409 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑛 ≼ 𝐵) |
13 | | simprr 522 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝐵 ≈ 𝑚) |
14 | | domentr 6751 |
. . . . . . . 8
⊢ ((𝑛 ≼ 𝐵 ∧ 𝐵 ≈ 𝑚) → 𝑛 ≼ 𝑚) |
15 | 12, 13, 14 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑛 ≼ 𝑚) |
16 | | simplrl 525 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑛 ∈ ω) |
17 | | simprl 521 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑚 ∈ ω) |
18 | | nndomo 6824 |
. . . . . . . 8
⊢ ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → (𝑛 ≼ 𝑚 ↔ 𝑛 ⊆ 𝑚)) |
19 | 16, 17, 18 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → (𝑛 ≼ 𝑚 ↔ 𝑛 ⊆ 𝑚)) |
20 | 15, 19 | mpbid 146 |
. . . . . 6
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑛 ⊆ 𝑚) |
21 | 13 | ensymd 6743 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑚 ≈ 𝐵) |
22 | | simprr 522 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐵 ≼ 𝐴) |
23 | 22 | ad2antrr 480 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝐵 ≼ 𝐴) |
24 | | endomtr 6750 |
. . . . . . . . 9
⊢ ((𝑚 ≈ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝑚 ≼ 𝐴) |
25 | 21, 23, 24 | syl2anc 409 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑚 ≼ 𝐴) |
26 | | domentr 6751 |
. . . . . . . 8
⊢ ((𝑚 ≼ 𝐴 ∧ 𝐴 ≈ 𝑛) → 𝑚 ≼ 𝑛) |
27 | 25, 7, 26 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑚 ≼ 𝑛) |
28 | | nndomo 6824 |
. . . . . . . 8
⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ≼ 𝑛 ↔ 𝑚 ⊆ 𝑛)) |
29 | 17, 16, 28 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → (𝑚 ≼ 𝑛 ↔ 𝑚 ⊆ 𝑛)) |
30 | 27, 29 | mpbid 146 |
. . . . . 6
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑚 ⊆ 𝑛) |
31 | 20, 30 | eqssd 3157 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝑛 = 𝑚) |
32 | 7, 31 | breqtrd 4005 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝐴 ≈ 𝑚) |
33 | | entr 6744 |
. . . 4
⊢ ((𝐴 ≈ 𝑚 ∧ 𝑚 ≈ 𝐵) → 𝐴 ≈ 𝐵) |
34 | 32, 21, 33 | syl2anc 409 |
. . 3
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
(𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ (𝑚 ∈ ω ∧ 𝐵 ≈ 𝑚)) → 𝐴 ≈ 𝐵) |
35 | 6, 34 | rexlimddv 2586 |
. 2
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → 𝐴 ≈ 𝐵) |
36 | 3, 35 | rexlimddv 2586 |
1
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵) |