Theorem onnmin

Description: No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997)

	Ref	Expression
Assertion	onnmin	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 ∈ ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		intss1	⊢ ( 𝐵 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝐵 )
2	1	adantl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴 ) → ∩ 𝐴 ⊆ 𝐵 )
3		ne0i	⊢ ( 𝐵 ∈ 𝐴 → 𝐴 ≠ ∅ )
4		oninton	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ On )
5	3 4	sylan2	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴 ) → ∩ 𝐴 ∈ On )
6		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ On )
7		ontri1	⊢ ( ( ∩ 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∩ 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ∩ 𝐴 ) )
8	5 6 7	syl2anc	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴 ) → ( ∩ 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ∩ 𝐴 ) )
9	2 8	mpbid	⊢ ( ( 𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 ∈ ∩ 𝐴 )