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	|- ( ( A C_ On /\ A =/= (/) ) -> inf ( A , On , _E ) = |^| A )

Proof

Step	Hyp	Ref	Expression
1		epweon	|- _E We On
2		weso	|- ( _E We On -> _E Or On )
3	1 2	mp1i	|- ( ( A C_ On /\ A =/= (/) ) -> _E Or On )
4		oninton	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )
5		onint	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )
6		intss1	|- ( x e. A -> |^| A C_ x )
7	6	adantl	|- ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> |^| A C_ x )
8		simpl	|- ( ( A C_ On /\ A =/= (/) ) -> A C_ On )
9	8	sselda	|- ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> x e. On )
10		ontri1	|- ( ( |^| A e. On /\ x e. On ) -> ( |^| A C_ x <-> -. x e. |^| A ) )
11	4 9 10	syl2an2r	|- ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> ( |^| A C_ x <-> -. x e. |^| A ) )
12	7 11	mpbid	|- ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> -. x e. |^| A )
13		epelg	|- ( |^| A e. On -> ( x _E |^| A <-> x e. |^| A ) )
14	4 13	syl	|- ( ( A C_ On /\ A =/= (/) ) -> ( x _E |^| A <-> x e. |^| A ) )
15	14	adantr	|- ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> ( x _E |^| A <-> x e. |^| A ) )
16	12 15	mtbird	|- ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> -. x _E |^| A )
17	3 4 5 16	infmin	|- ( ( A C_ On /\ A =/= (/) ) -> inf ( A , On , _E ) = |^| A )