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 ( 𝐵 ⊆ On → ( ( 𝐴𝐵 ∧ ∀ 𝑥𝐴 ¬ 𝑥𝐵 ) → 𝐴 = 𝐵 ) )

Proof

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