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