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 e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( ( A \ B ) ~<_ B <-> A ~<_ B ) )

Proof

Step	Hyp	Ref	Expression
1		domnsym	|- ( ( A \ B ) ~<_ B -> -. B ~< ( A \ B ) )
2		simp3	|- ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> B ~< A )
3		infdif	|- ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A \ B ) ~~ A )
4	3	ensymd	|- ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> A ~~ ( A \ B ) )
5		sdomentr	|- ( ( B ~< A /\ A ~~ ( A \ B ) ) -> B ~< ( A \ B ) )
6	2 4 5	syl2anc	|- ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> B ~< ( A \ B ) )
7	1 6	nsyl3	|- ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> -. ( A \ B ) ~<_ B )
8	7	3expia	|- ( ( A e. dom card /\ _om ~<_ A ) -> ( B ~< A -> -. ( A \ B ) ~<_ B ) )
9	8	3adant2	|- ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( B ~< A -> -. ( A \ B ) ~<_ B ) )
10	9	con2d	|- ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( ( A \ B ) ~<_ B -> -. B ~< A ) )
11		domtri2	|- ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) )
12	11	3adant3	|- ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A ~<_ B <-> -. B ~< A ) )
13	10 12	sylibrd	|- ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( ( A \ B ) ~<_ B -> A ~<_ B ) )
14		simp1	|- ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> A e. dom card )
15		difss	|- ( A \ B ) C_ A
16		ssdomg	|- ( A e. dom card -> ( ( A \ B ) C_ A -> ( A \ B ) ~<_ A ) )
17	14 15 16	mpisyl	|- ( ( A e. dom card /\ B e. dom card /\ _om ~<_ 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 e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A ~<_ B -> ( A \ B ) ~<_ B ) )
21	13 20	impbid	|- ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( ( A \ B ) ~<_ B <-> A ~<_ B ) )