Theorem onsupnmax

Description: If the union of a class of ordinals is not the maximum element of that class, then the union is a limit ordinal or empty. But this isn't a biconditional since A could be a non-empty set where a limit ordinal or the empty set happens to be the largest element. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupnmax	|- ( A C_ On -> ( -. U. A e. A -> U. A = U. U. A ) )

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		simpll	|- ( ( ( A C_ On /\ U. A e. On ) /\ x e. A ) -> A C_ On )
8	7	sselda	|- ( ( ( ( A C_ On /\ U. A e. On ) /\ x e. A ) /\ y e. A ) -> y e. On )
9		simpl	|- ( ( A C_ On /\ U. A e. On ) -> A C_ On )
10	9	sselda	|- ( ( ( A C_ On /\ U. A e. On ) /\ x e. A ) -> x e. On )
11	10	adantr	|- ( ( ( ( A C_ On /\ U. A e. On ) /\ x e. A ) /\ y e. A ) -> x e. On )
12		ontri1	|- ( ( y e. On /\ x e. On ) -> ( y C_ x <-> -. x e. y ) )
13	8 11 12	syl2anc	|- ( ( ( ( A C_ On /\ U. A e. On ) /\ x e. A ) /\ y e. A ) -> ( y C_ x <-> -. x e. y ) )
14	13	ralbidva	|- ( ( ( A C_ On /\ U. A e. On ) /\ x e. A ) -> ( A. y e. A y C_ x <-> A. y e. A -. x e. y ) )
15	14	rexbidva	|- ( ( A C_ On /\ U. A e. On ) -> ( E. x e. A A. y e. A y C_ x <-> E. x e. A A. y e. A -. x e. y ) )
16	6 15	bitr4id	|- ( ( A C_ On /\ U. A e. On ) -> ( -. A C_ U. A <-> E. x e. A A. y e. A y C_ x ) )
17		unielid	|- ( U. A e. A <-> E. x e. A A. y e. A y C_ x )
18	17	a1i	|- ( ( A C_ On /\ U. A e. On ) -> ( U. A e. A <-> E. x e. A A. y e. A y C_ x ) )
19	18	biimprd	|- ( ( A C_ On /\ U. A e. On ) -> ( E. x e. A A. y e. A y C_ x -> U. A e. A ) )
20	16 19	sylbid	|- ( ( A C_ On /\ U. A e. On ) -> ( -. A C_ U. A -> U. A e. A ) )
21	20	con1d	|- ( ( A C_ On /\ U. A e. On ) -> ( -. U. A e. A -> A C_ U. A ) )
22		uniss	|- ( A C_ U. A -> U. A C_ U. U. A )
23	21 22	syl6	|- ( ( A C_ On /\ U. A e. On ) -> ( -. U. A e. A -> U. A C_ U. U. A ) )
24		ssorduni	|- ( A C_ On -> Ord U. A )
25		orduniss	|- ( Ord U. A -> U. U. A C_ U. A )
26	24 25	syl	|- ( A C_ On -> U. U. A C_ U. A )
27	26	biantrud	|- ( A C_ On -> ( U. A C_ U. U. A <-> ( U. A C_ U. U. A /\ U. U. A C_ U. A ) ) )
28		eqss	|- ( U. A = U. U. A <-> ( U. A C_ U. U. A /\ U. U. A C_ U. A ) )
29	27 28	bitr4di	|- ( A C_ On -> ( U. A C_ U. U. A <-> U. A = U. U. A ) )
30	29	adantr	|- ( ( A C_ On /\ U. A e. On ) -> ( U. A C_ U. U. A <-> U. A = U. U. A ) )
31	23 30	sylibd	|- ( ( A C_ On /\ U. A e. On ) -> ( -. U. A e. A -> U. A = U. U. A ) )
32	31	ex	|- ( A C_ On -> ( U. A e. On -> ( -. U. A e. A -> U. A = U. U. A ) ) )
33		unon	|- U. On = On
34	33	a1i	|- ( U. A = On -> U. On = On )
35		unieq	|- ( U. A = On -> U. U. A = U. On )
36		id	|- ( U. A = On -> U. A = On )
37	34 35 36	3eqtr4rd	|- ( U. A = On -> U. A = U. U. A )
38	37	a1i13	|- ( A C_ On -> ( U. A = On -> ( -. U. A e. A -> U. A = U. U. A ) ) )
39		ordeleqon	|- ( Ord U. A <-> ( U. A e. On \/ U. A = On ) )
40	24 39	sylib	|- ( A C_ On -> ( U. A e. On \/ U. A = On ) )
41	32 38 40	mpjaod	|- ( A C_ On -> ( -. U. A e. A -> U. A = U. U. A ) )