Metamath Proof Explorer

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 ⊢ B ⊆ On ∧ B ≠ ∅ → A = ⋂ B ↔ A ∈ B ∧ ∀ x ∈ A ¬ x ∈ B

Proof

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