Theorem ordeldif

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

	Ref	Expression
Assertion	ordeldif	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐵 ) )
2		simpr	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord 𝐵 )
3		ordelord	⊢ ( ( Ord 𝐴 ∧ 𝐶 ∈ 𝐴 ) → Ord 𝐶 )
4	3	adantlr	⊢ ( ( ( Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → Ord 𝐶 )
5		ordtri1	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝐵 ) )
6	2 4 5	syl2an2r	⊢ ( ( ( Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝐵 ) )
7	6	bicomd	⊢ ( ( ( Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( ¬ 𝐶 ∈ 𝐵 ↔ 𝐵 ⊆ 𝐶 ) )
8	7	pm5.32da	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶 ) ) )
9	1 8	bitrid	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶 ) ) )