Step |
Hyp |
Ref |
Expression |
1 |
|
domnsym |
⊢ ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴 ) |
2 |
|
finnum |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card ) |
3 |
2
|
adantr |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ dom card ) |
4 |
|
finnum |
⊢ ( 𝐵 ∈ Fin → 𝐵 ∈ dom card ) |
5 |
|
domtri2 |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐵 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) ) |
7 |
6
|
biimprd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐵 ∈ Fin ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) ) |
8 |
|
isinffi |
⊢ ( ( ¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 ) |
9 |
8
|
ancoms |
⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 ) |
10 |
9
|
adantlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 ) |
11 |
|
brdomg |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 ) ) |
12 |
11
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 ) ) |
13 |
10 12
|
mpbird |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → 𝐴 ≼ 𝐵 ) |
14 |
13
|
a1d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) ) |
15 |
7 14
|
pm2.61dan |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) ) |
16 |
1 15
|
impbid2 |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) ) |