Description: The domain of a one-to-one function is dominated by its codomain. This variation of f1domg does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015) (Proof shortened by BTernaryTau, 25-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | f1dom2g | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1f | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 ) | |
| 2 | fex2 | ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐹 ∈ V ) | |
| 3 | 1 2 | syl3an1 | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐹 ∈ V ) |
| 4 | 3 | 3coml | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ V ) |
| 5 | f1dom3g | ⊢ ( ( 𝐹 ∈ V ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 ) | |
| 6 | 4 5 | syld3an1 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 ) |