Theorem oninfint

Description: The infimum of a non-empty class of ordinals is the intersection of that class. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	oninfint	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → inf ( 𝐴 , On , E ) = ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		epweon	⊢ E We On
2		weso	⊢ ( E We On → E Or On )
3	1 2	mp1i	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → E Or On )
4		oninton	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ On )
5		onint	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )
6		intss1	⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥 )
7	6	adantl	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ∩ 𝐴 ⊆ 𝑥 )
8		simpl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ On )
9	8	sselda	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
10		ontri1	⊢ ( ( ∩ 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∩ 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ∩ 𝐴 ) )
11	4 9 10	syl2an2r	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∩ 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ∩ 𝐴 ) )
12	7 11	mpbid	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ ∩ 𝐴 )
13		epelg	⊢ ( ∩ 𝐴 ∈ On → ( 𝑥 E ∩ 𝐴 ↔ 𝑥 ∈ ∩ 𝐴 ) )
14	4 13	syl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( 𝑥 E ∩ 𝐴 ↔ 𝑥 ∈ ∩ 𝐴 ) )
15	14	adantr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 E ∩ 𝐴 ↔ 𝑥 ∈ ∩ 𝐴 ) )
16	12 15	mtbird	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 E ∩ 𝐴 )
17	3 4 5 16	infmin	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → inf ( 𝐴 , On , E ) = ∩ 𝐴 )