Metamath Proof Explorer

Theorem infdif2

Description: Cardinality ordering for an infinite class difference. (Contributed by NM, 24-Mar-2007) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infdif2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ∖ B ≼ B ↔ A ≼ B

Proof

Step Hyp Ref Expression
1 domnsym ⊢ A ∖ B ≼ B → ¬ B ≺ A ∖ B
2 simp3 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≺ A → B ≺ A
3 infdif ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≺ A → A ∖ B ≈ A
4 3 ensymd ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≺ A → A ≈ A ∖ B
5 sdomentr ⊢ B ≺ A ∧ A ≈ A ∖ B → B ≺ A ∖ B
6 2 4 5 syl2anc ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≺ A → B ≺ A ∖ B
7 1 6 nsyl3 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≺ A → ¬ A ∖ B ≼ B
8 7 3expia ⊢ A ∈ dom ⁡ card ∧ ω ≼ A → B ≺ A → ¬ A ∖ B ≼ B
9 8 3adant2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → B ≺ A → ¬ A ∖ B ≼ B
10 9 con2d ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ∖ B ≼ B → ¬ B ≺ A
11 domtri2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ≼ B ↔ ¬ B ≺ A
12 11 3adant3 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ≼ B ↔ ¬ B ≺ A
13 10 12 sylibrd ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ∖ B ≼ B → A ≼ B
14 simp1 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ∈ dom ⁡ card
15 difss ⊢ A ∖ B ⊆ A
16 ssdomg ⊢ A ∈ dom ⁡ card → A ∖ B ⊆ A → A ∖ B ≼ A
17 14 15 16 mpisyl ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ∖ B ≼ A
18 domtr ⊢ A ∖ B ≼ A ∧ A ≼ B → A ∖ B ≼ B
19 18 ex ⊢ A ∖ B ≼ A → A ≼ B → A ∖ B ≼ B
20 17 19 syl ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ≼ B → A ∖ B ≼ B
21 13 20 impbid ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ∖ B ≼ B ↔ A ≼ B