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 | ⊢ ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 ) |
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 | ⊢ ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 ) |