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 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( 𝐴 ∖ 𝐵 ) ≼ 𝐵 ↔ 𝐴 ≼ 𝐵 ) )

Proof

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