Theorem onmindif

Description: When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003)

	Ref	Expression
Assertion	onmindif	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ On ) → 𝐵 ∈ ∩ ( 𝐴 ∖ suc 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ suc 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ suc 𝐵 ) )
2		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
3		ontri1	⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝑥 ) )
4		onsssuc	⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵 ) )
5	3 4	bitr3d	⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝐵 ∈ 𝑥 ↔ 𝑥 ∈ suc 𝐵 ) )
6	5	con1bid	⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝑥 ∈ suc 𝐵 ↔ 𝐵 ∈ 𝑥 ) )
7	2 6	sylan	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ∈ On ) → ( ¬ 𝑥 ∈ suc 𝐵 ↔ 𝐵 ∈ 𝑥 ) )
8	7	biimpd	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ∈ On ) → ( ¬ 𝑥 ∈ suc 𝐵 → 𝐵 ∈ 𝑥 ) )
9	8	exp31	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ On → ( ¬ 𝑥 ∈ suc 𝐵 → 𝐵 ∈ 𝑥 ) ) ) )
10	9	com23	⊢ ( 𝐴 ⊆ On → ( 𝐵 ∈ On → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ suc 𝐵 → 𝐵 ∈ 𝑥 ) ) ) )
11	10	imp4b	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ suc 𝐵 ) → 𝐵 ∈ 𝑥 ) )
12	1 11	syl5bi	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ On ) → ( 𝑥 ∈ ( 𝐴 ∖ suc 𝐵 ) → 𝐵 ∈ 𝑥 ) )
13	12	ralrimiv	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ On ) → ∀ 𝑥 ∈ ( 𝐴 ∖ suc 𝐵 ) 𝐵 ∈ 𝑥 )
14		elintg	⊢ ( 𝐵 ∈ On → ( 𝐵 ∈ ∩ ( 𝐴 ∖ suc 𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ suc 𝐵 ) 𝐵 ∈ 𝑥 ) )
15	14	adantl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ On ) → ( 𝐵 ∈ ∩ ( 𝐴 ∖ suc 𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ suc 𝐵 ) 𝐵 ∈ 𝑥 ) )
16	13 15	mpbird	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ On ) → 𝐵 ∈ ∩ ( 𝐴 ∖ suc 𝐵 ) )