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

Metamath Proof Explorer

Theorem domwdom

Description: Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Assertion domwdom ( 𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌 )

Proof

Step Hyp Ref Expression
1 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
2 1 adantl ⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
3 reldom ⊢ Rel ≼
4 3 brrelex1i ⊢ ( 𝑋 ≼ 𝑌 → 𝑋 ∈ V )
5 0sdomg ⊢ ( 𝑋 ∈ V → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
6 4 5 syl ⊢ ( 𝑋 ≼ 𝑌 → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
7 6 adantr ⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
8 2 7 mpbird ⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → ∅ ≺ 𝑋 )
9 simpl ⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≼ 𝑌 )
10 fodomr ⊢ ( ( ∅ ≺ 𝑋 ∧ 𝑋 ≼ 𝑌 ) → ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 )
11 8 9 10 syl2anc ⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 )
12 11 ex ⊢ ( 𝑋 ≼ 𝑌 → ( ¬ 𝑋 = ∅ → ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) )
13 12 orrd ⊢ ( 𝑋 ≼ 𝑌 → ( 𝑋 = ∅ ∨ ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) )
14 3 brrelex2i ⊢ ( 𝑋 ≼ 𝑌 → 𝑌 ∈ V )
15 brwdom ⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) ) )
16 14 15 syl ⊢ ( 𝑋 ≼ 𝑌 → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) ) )
17 13 16 mpbird ⊢ ( 𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌 )