Metamath Proof Explorer


Theorem wdomac

Description: When assuming AC, weak and usual dominance coincide. It is not known if this is an AC equivalent. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion wdomac ( 𝑋* 𝑌𝑋𝑌 )

Proof

Step Hyp Ref Expression
1 relwdom Rel ≼*
2 1 brrelex2i ( 𝑋* 𝑌𝑌 ∈ V )
3 reldom Rel ≼
4 3 brrelex2i ( 𝑋𝑌𝑌 ∈ V )
5 numth3 ( 𝑌 ∈ V → 𝑌 ∈ dom card )
6 wdomnumr ( 𝑌 ∈ dom card → ( 𝑋* 𝑌𝑋𝑌 ) )
7 5 6 syl ( 𝑌 ∈ V → ( 𝑋* 𝑌𝑋𝑌 ) )
8 2 4 7 pm5.21nii ( 𝑋* 𝑌𝑋𝑌 )