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

Metamath Proof Explorer

Theorem brwdomn0

Description: Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion brwdomn0 ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 relwdom ⊢ Rel ≼*
2 1 brrelex2i ⊢ ( 𝑋 ≼* 𝑌 → 𝑌 ∈ V )
3 2 a1i ⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 → 𝑌 ∈ V ) )
4 fof ⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → 𝑧 : 𝑌 ⟶ 𝑋 )
5 4 fdmd ⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → dom 𝑧 = 𝑌 )
6 vex ⊢ 𝑧 ∈ V
7 6 dmex ⊢ dom 𝑧 ∈ V
8 5 7 eqeltrrdi ⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → 𝑌 ∈ V )
9 8 exlimiv ⊢ ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 → 𝑌 ∈ V )
10 9 a1i ⊢ ( 𝑋 ≠ ∅ → ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 → 𝑌 ∈ V ) )
11 brwdom ⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
12 df-ne ⊢ ( 𝑋 ≠ ∅ ↔ ¬ 𝑋 = ∅ )
13 biorf ⊢ ( ¬ 𝑋 = ∅ → ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
14 12 13 sylbi ⊢ ( 𝑋 ≠ ∅ → ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
15 14 bicomd ⊢ ( 𝑋 ≠ ∅ → ( ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
16 11 15 sylan9bbr ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ∈ V ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
17 16 ex ⊢ ( 𝑋 ≠ ∅ → ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
18 3 10 17 pm5.21ndd ⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )