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

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