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𝑋 ) )