Metamath Proof Explorer

Theorem wdomnumr

Description: Weak dominance agrees with normal for numerable right sets. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion wdomnumr ⊢ B ∈ dom ⁡ card → A ≼ * B ↔ A ≼ B

Proof

Step Hyp Ref Expression
1 brwdom ⊢ B ∈ dom ⁡ card → A ≼ * B ↔ A = ∅ ∨ ∃ x x : B ⟶ onto A
2 0domg ⊢ B ∈ dom ⁡ card → ∅ ≼ B
3 breq1 ⊢ A = ∅ → A ≼ B ↔ ∅ ≼ B
4 2 3 syl5ibrcom ⊢ B ∈ dom ⁡ card → A = ∅ → A ≼ B
5 fodomnum ⊢ B ∈ dom ⁡ card → x : B ⟶ onto A → A ≼ B
6 5 exlimdv ⊢ B ∈ dom ⁡ card → ∃ x x : B ⟶ onto A → A ≼ B
7 4 6 jaod ⊢ B ∈ dom ⁡ card → A = ∅ ∨ ∃ x x : B ⟶ onto A → A ≼ B
8 1 7 sylbid ⊢ B ∈ dom ⁡ card → A ≼ * B → A ≼ B
9 domwdom ⊢ A ≼ B → A ≼ * B
10 8 9 impbid1 ⊢ B ∈ dom ⁡ card → A ≼ * B ↔ A ≼ B