Theorem ordeldif

Description: Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025)

	Ref	Expression
Assertion	ordeldif	|- ( ( Ord A /\ Ord B ) -> ( C e. ( A \ B ) <-> ( C e. A /\ B C_ C ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( C e. ( A \ B ) <-> ( C e. A /\ -. C e. B ) )
2		simpr	|- ( ( Ord A /\ Ord B ) -> Ord B )
3		ordelord	|- ( ( Ord A /\ C e. A ) -> Ord C )
4	3	adantlr	|- ( ( ( Ord A /\ Ord B ) /\ C e. A ) -> Ord C )
5		ordtri1	|- ( ( Ord B /\ Ord C ) -> ( B C_ C <-> -. C e. B ) )
6	2 4 5	syl2an2r	|- ( ( ( Ord A /\ Ord B ) /\ C e. A ) -> ( B C_ C <-> -. C e. B ) )
7	6	bicomd	|- ( ( ( Ord A /\ Ord B ) /\ C e. A ) -> ( -. C e. B <-> B C_ C ) )
8	7	pm5.32da	|- ( ( Ord A /\ Ord B ) -> ( ( C e. A /\ -. C e. B ) <-> ( C e. A /\ B C_ C ) ) )
9	1 8	bitrid	|- ( ( Ord A /\ Ord B ) -> ( C e. ( A \ B ) <-> ( C e. A /\ B C_ C ) ) )