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