This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fodomnum

Description: A version of fodom that doesn't require the Axiom of Choice ax-ac . (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fodomnum ⊢ A ∈ dom ⁡ card → F : A ⟶ onto B → B ≼ A

Proof

Step Hyp Ref Expression
1 focdmex ⊢ A ∈ dom ⁡ card → F : A ⟶ onto B → B ∈ V
2 1 com12 ⊢ F : A ⟶ onto B → A ∈ dom ⁡ card → B ∈ V
3 numacn ⊢ B ∈ V → A ∈ dom ⁡ card → A ∈ AC _ B
4 2 3 syli ⊢ F : A ⟶ onto B → A ∈ dom ⁡ card → A ∈ AC _ B
5 4 com12 ⊢ A ∈ dom ⁡ card → F : A ⟶ onto B → A ∈ AC _ B
6 fodomacn ⊢ A ∈ AC _ B → F : A ⟶ onto B → B ≼ A
7 5 6 syli ⊢ A ∈ dom ⁡ card → F : A ⟶ onto B → B ≼ A