Metamath Proof Explorer

Theorem oneqmini

Description: A way to show that an ordinal number equals the minimum of a 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 oneqmini ⊢ B ⊆ On → A ∈ B ∧ ∀ x ∈ A ¬ x ∈ B → A = ⋂ B

Proof

Step Hyp Ref Expression
1 ssint ⊢ A ⊆ ⋂ B ↔ ∀ x ∈ B A ⊆ x
2 ssel ⊢ B ⊆ On → A ∈ B → A ∈ On
3 ssel ⊢ B ⊆ On → x ∈ B → x ∈ On
4 2 3 anim12d ⊢ B ⊆ On → A ∈ B ∧ x ∈ B → A ∈ On ∧ x ∈ On
5 ontri1 ⊢ A ∈ On ∧ x ∈ On → A ⊆ x ↔ ¬ x ∈ A
6 4 5 syl6 ⊢ B ⊆ On → A ∈ B ∧ x ∈ B → A ⊆ x ↔ ¬ x ∈ A
7 6 expdimp ⊢ B ⊆ On ∧ A ∈ B → x ∈ B → A ⊆ x ↔ ¬ x ∈ A
8 7 pm5.74d ⊢ B ⊆ On ∧ A ∈ B → x ∈ B → A ⊆ x ↔ x ∈ B → ¬ x ∈ A
9 con2b ⊢ x ∈ B → ¬ x ∈ A ↔ x ∈ A → ¬ x ∈ B
10 8 9 bitrdi ⊢ B ⊆ On ∧ A ∈ B → x ∈ B → A ⊆ x ↔ x ∈ A → ¬ x ∈ B
11 10 ralbidv2 ⊢ B ⊆ On ∧ A ∈ B → ∀ x ∈ B A ⊆ x ↔ ∀ x ∈ A ¬ x ∈ B
12 1 11 bitrid ⊢ B ⊆ On ∧ A ∈ B → A ⊆ ⋂ B ↔ ∀ x ∈ A ¬ x ∈ B
13 12 biimprd ⊢ B ⊆ On ∧ A ∈ B → ∀ x ∈ A ¬ x ∈ B → A ⊆ ⋂ B
14 13 expimpd ⊢ B ⊆ On → A ∈ B ∧ ∀ x ∈ A ¬ x ∈ B → A ⊆ ⋂ B
15 intss1 ⊢ A ∈ B → ⋂ B ⊆ A
16 15 a1i ⊢ B ⊆ On → A ∈ B → ⋂ B ⊆ A
17 16 adantrd ⊢ B ⊆ On → A ∈ B ∧ ∀ x ∈ A ¬ x ∈ B → ⋂ B ⊆ A
18 14 17 jcad ⊢ B ⊆ On → A ∈ B ∧ ∀ x ∈ A ¬ x ∈ B → A ⊆ ⋂ B ∧ ⋂ B ⊆ A
19 eqss ⊢ A = ⋂ B ↔ A ⊆ ⋂ B ∧ ⋂ B ⊆ A
20 18 19 imbitrrdi ⊢ B ⊆ On → A ∈ B ∧ ∀ x ∈ A ¬ x ∈ B → A = ⋂ B