Step |
Hyp |
Ref |
Expression |
1 |
|
carddom2 |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |
2 |
|
cardon |
⊢ ( card ‘ 𝐴 ) ∈ On |
3 |
|
cardon |
⊢ ( card ‘ 𝐵 ) ∈ On |
4 |
|
ontri1 |
⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ) ) |
5 |
2 3 4
|
mp2an |
⊢ ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ) |
6 |
|
cardsdom2 |
⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ↔ 𝐵 ≺ 𝐴 ) ) |
7 |
6
|
ancoms |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ↔ 𝐵 ≺ 𝐴 ) ) |
8 |
7
|
notbid |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ↔ ¬ 𝐵 ≺ 𝐴 ) ) |
9 |
5 8
|
syl5bb |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ 𝐵 ≺ 𝐴 ) ) |
10 |
1 9
|
bitr3d |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) ) |