This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐵 ⊆ 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 ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∩ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) ) )