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