Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C ( x ) and D ( y ) , as can be inferred from their distinct variable conditions. (Contributed by Mario Carneiro, 20-May-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dom2.1 | ⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) | |
| dom2.2 | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) | ||
| Assertion | dom3 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ≼ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dom2.1 | ⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) | |
| 2 | dom2.2 | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) | |
| 3 | 1 | a1i | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) ) |
| 4 | 2 | a1i | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝑥 = 𝑦 ) ) ) |
| 5 | simpl | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 ) | |
| 6 | simpr | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 ) | |
| 7 | 3 4 5 6 | dom3d | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ≼ 𝐵 ) |