Theorem onmaxnelsup

Description: Two ways to say the maximum element of a class of ordinals is also the supremum of that class. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onmaxnelsup	|- ( A C_ On -> ( -. A C_ U. A <-> E. x e. A A. y e. A y C_ x ) )

Proof

Step	Hyp	Ref	Expression
1		rexnal	|- ( E. x e. A -. E. y e. A x e. y <-> -. A. x e. A E. y e. A x e. y )
2		ralnex	|- ( A. y e. A -. x e. y <-> -. E. y e. A x e. y )
3	2	rexbii	|- ( E. x e. A A. y e. A -. x e. y <-> E. x e. A -. E. y e. A x e. y )
4		ssunib	|- ( A C_ U. A <-> A. x e. A E. y e. A x e. y )
5	4	notbii	|- ( -. A C_ U. A <-> -. A. x e. A E. y e. A x e. y )
6	1 3 5	3bitr4ri	|- ( -. A C_ U. A <-> E. x e. A A. y e. A -. x e. y )
7		simpl	|- ( ( A C_ On /\ x e. A ) -> A C_ On )
8	7	sselda	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> y e. On )
9		ssel2	|- ( ( A C_ On /\ x e. A ) -> x e. On )
10	9	adantr	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> x e. On )
11		ontri1	|- ( ( y e. On /\ x e. On ) -> ( y C_ x <-> -. x e. y ) )
12	8 10 11	syl2anc	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> ( y C_ x <-> -. x e. y ) )
13	12	ralbidva	|- ( ( A C_ On /\ x e. A ) -> ( A. y e. A y C_ x <-> A. y e. A -. x e. y ) )
14	13	rexbidva	|- ( A C_ On -> ( E. x e. A A. y e. A y C_ x <-> E. x e. A A. y e. A -. x e. y ) )
15	6 14	bitr4id	|- ( A C_ On -> ( -. A C_ U. A <-> E. x e. A A. y e. A y C_ x ) )