Theorem oneqmin

Description: A way to show that an ordinal number equals the minimum of a nonempty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003)

	Ref	Expression
Assertion	oneqmin	⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		onint	⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ∩ 𝐵 ∈ 𝐵 )
2		eleq1	⊢ ( 𝐴 = ∩ 𝐵 → ( 𝐴 ∈ 𝐵 ↔ ∩ 𝐵 ∈ 𝐵 ) )
3	1 2	syl5ibrcom	⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 → 𝐴 ∈ 𝐵 ) )
4		eleq2	⊢ ( 𝐴 = ∩ 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ∩ 𝐵 ) )
5	4	biimpd	⊢ ( 𝐴 = ∩ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∩ 𝐵 ) )
6		onnmin	⊢ ( ( 𝐵 ⊆ On ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ∩ 𝐵 )
7	6	ex	⊢ ( 𝐵 ⊆ On → ( 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ ∩ 𝐵 ) )
8	7	con2d	⊢ ( 𝐵 ⊆ On → ( 𝑥 ∈ ∩ 𝐵 → ¬ 𝑥 ∈ 𝐵 ) )
9	5 8	syl9r	⊢ ( 𝐵 ⊆ On → ( 𝐴 = ∩ 𝐵 → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ) )
10	9	ralrimdv	⊢ ( 𝐵 ⊆ On → ( 𝐴 = ∩ 𝐵 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) )
11	10	adantr	⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) )
12	3 11	jcad	⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 → ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) )
13		oneqmini	⊢ ( 𝐵 ⊆ On → ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) → 𝐴 = ∩ 𝐵 ) )
14	13	adantr	⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) → 𝐴 = ∩ 𝐵 ) )
15	12 14	impbid	⊢ ( ( 𝐵 ⊆ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) )