Description: Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | domen2 | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | domentr | ⊢ ( ( 𝐶 ≼ 𝐴 ∧ 𝐴 ≈ 𝐵 ) → 𝐶 ≼ 𝐵 ) | |
2 | 1 | ancoms | ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≼ 𝐴 ) → 𝐶 ≼ 𝐵 ) |
3 | ensym | ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 ) | |
4 | domentr | ⊢ ( ( 𝐶 ≼ 𝐵 ∧ 𝐵 ≈ 𝐴 ) → 𝐶 ≼ 𝐴 ) | |
5 | 4 | ancoms | ⊢ ( ( 𝐵 ≈ 𝐴 ∧ 𝐶 ≼ 𝐵 ) → 𝐶 ≼ 𝐴 ) |
6 | 3 5 | sylan | ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≼ 𝐵 ) → 𝐶 ≼ 𝐴 ) |
7 | 2 6 | impbida | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵 ) ) |