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

Metamath Proof Explorer

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→ 𝑋 ) → 𝑋 ≼* 𝑌 )