Theorem onsupeqnmax

Description: Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupeqnmax	|- ( A C_ On -> ( A. x e. A E. y e. A x e. y <-> ( U. A = U. U. A /\ -. U. A e. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A C_ On /\ x e. A ) -> A C_ On )
2	1	sselda	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> y e. On )
3		ssel2	|- ( ( A C_ On /\ x e. A ) -> x e. On )
4	3	adantr	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> x e. On )
5		ontri1	|- ( ( y e. On /\ x e. On ) -> ( y C_ x <-> -. x e. y ) )
6	2 4 5	syl2anc	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> ( y C_ x <-> -. x e. y ) )
7	6	ralbidva	|- ( ( A C_ On /\ x e. A ) -> ( A. y e. A y C_ x <-> A. y e. A -. x e. y ) )
8	7	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 ) )
9	8	notbid	|- ( 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 ) )
10	9	bicomd	|- ( A C_ On -> ( -. E. x e. A A. y e. A -. x e. y <-> -. E. x e. A A. y e. A y C_ x ) )
11		dfrex2	|- ( E. y e. A x e. y <-> -. A. y e. A -. x e. y )
12	11	ralbii	|- ( A. x e. A E. y e. A x e. y <-> A. x e. A -. A. y e. A -. x e. y )
13		ralnex	|- ( A. x e. A -. A. y e. A -. x e. y <-> -. E. x e. A A. y e. A -. x e. y )
14	12 13	bitri	|- ( A. x e. A E. y e. A x e. y <-> -. E. x e. A A. y e. A -. x e. y )
15		unielid	|- ( U. A e. A <-> E. x e. A A. y e. A y C_ x )
16	15	notbii	|- ( -. U. A e. A <-> -. E. x e. A A. y e. A y C_ x )
17	10 14 16	3bitr4g	|- ( A C_ On -> ( A. x e. A E. y e. A x e. y <-> -. U. A e. A ) )
18		onsupnmax	|- ( A C_ On -> ( -. U. A e. A -> U. A = U. U. A ) )
19	18	pm4.71rd	|- ( A C_ On -> ( -. U. A e. A <-> ( U. A = U. U. A /\ -. U. A e. A ) ) )
20	17 19	bitrd	|- ( A C_ On -> ( A. x e. A E. y e. A x e. y <-> ( U. A = U. U. A /\ -. U. A e. A ) ) )