Theorem fowdom

Description: An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	fowdom	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → 𝑋 ≼* 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
2		foeq1	⊢ ( 𝑧 = 𝐹 → ( 𝑧 : 𝑌 –onto→ 𝑋 ↔ 𝐹 : 𝑌 –onto→ 𝑋 ) )
3	2	spcegv	⊢ ( 𝐹 ∈ V → ( 𝐹 : 𝑌 –onto→ 𝑋 → ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
4	3	imp	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 )
5	4	olcd	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
6		fof	⊢ ( 𝐹 : 𝑌 –onto→ 𝑋 → 𝐹 : 𝑌 ⟶ 𝑋 )
7		dmfex	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑌 ∈ V )
8	6 7	sylan2	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → 𝑌 ∈ V )
9		brwdom	⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
10	8 9	syl	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
11	5 10	mpbird	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → 𝑋 ≼* 𝑌 )
12	1 11	sylan	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → 𝑋 ≼* 𝑌 )