Theorem onsupmaxb

Description: The union of a class of ordinals is an element is an element of that class if and only if there is a maximum element of that class under the epsilon relation, which is to say that the domain of the restricted epsilon relation is not the whole class. (Contributed by RP, 25-Jan-2025)

	Ref	Expression
Assertion	onsupmaxb	|- ( A C_ On -> ( dom ( _E i^i ( A X. A ) ) = A <-> -. U. A e. A ) )

Proof

Step	Hyp	Ref	Expression
1		elirrv	|- -. x e. x
2		pm5.501	|- ( -. x e. x -> ( E. y e. A x e. y <-> ( -. x e. x <-> E. y e. A x e. y ) ) )
3	1 2	mp1i	|- ( z = x -> ( E. y e. A x e. y <-> ( -. x e. x <-> E. y e. A x e. y ) ) )
4		elequ1	|- ( z = x -> ( z e. x <-> x e. x ) )
5	4	notbid	|- ( z = x -> ( -. z e. x <-> -. x e. x ) )
6		elequ1	|- ( z = x -> ( z e. y <-> x e. y ) )
7	6	rexbidv	|- ( z = x -> ( E. y e. A z e. y <-> E. y e. A x e. y ) )
8	5 7	bibi12d	|- ( z = x -> ( ( -. z e. x <-> E. y e. A z e. y ) <-> ( -. x e. x <-> E. y e. A x e. y ) ) )
9	3 8	bitr4d	|- ( z = x -> ( E. y e. A x e. y <-> ( -. z e. x <-> E. y e. A z e. y ) ) )
10	9	biimpd	|- ( z = x -> ( E. y e. A x e. y -> ( -. z e. x <-> E. y e. A z e. y ) ) )
11	10	spimevw	|- ( E. y e. A x e. y -> E. z ( -. z e. x <-> E. y e. A z e. y ) )
12		ssel	|- ( A C_ On -> ( y e. A -> y e. On ) )
13	12	adantr	|- ( ( A C_ On /\ x e. A ) -> ( y e. A -> y e. On ) )
14	13	imp	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> y e. On )
15		ssel2	|- ( ( A C_ On /\ x e. A ) -> x e. On )
16	15	adantr	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> x e. On )
17		ontri1	|- ( ( y e. On /\ x e. On ) -> ( y C_ x <-> -. x e. y ) )
18	14 16 17	syl2anc	|- ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> ( y C_ x <-> -. x e. y ) )
19	18	ralbidva	|- ( ( A C_ On /\ x e. A ) -> ( A. y e. A y C_ x <-> A. y e. A -. x e. y ) )
20		ralnex	|- ( A. y e. A -. x e. y <-> -. E. y e. A x e. y )
21	19 20	bitrdi	|- ( ( A C_ On /\ x e. A ) -> ( A. y e. A y C_ x <-> -. E. y e. A x e. y ) )
22		unissb	|- ( U. A C_ x <-> A. y e. A y C_ x )
23		simpr	|- ( ( ( A C_ On /\ x e. A ) /\ U. A C_ x ) -> U. A C_ x )
24		elssuni	|- ( x e. A -> x C_ U. A )
25	24	ad2antlr	|- ( ( ( A C_ On /\ x e. A ) /\ U. A C_ x ) -> x C_ U. A )
26	23 25	eqssd	|- ( ( ( A C_ On /\ x e. A ) /\ U. A C_ x ) -> U. A = x )
27	22 26	sylan2br	|- ( ( ( A C_ On /\ x e. A ) /\ A. y e. A y C_ x ) -> U. A = x )
28		dfuni2	|- U. A = { z | E. y e. A z e. y }
29	28	eqeq1i	|- ( U. A = x <-> { z | E. y e. A z e. y } = x )
30		eqabcb	|- ( { z | E. y e. A z e. y } = x <-> A. z ( E. y e. A z e. y <-> z e. x ) )
31		bicom	|- ( ( E. y e. A z e. y <-> z e. x ) <-> ( z e. x <-> E. y e. A z e. y ) )
32	31	albii	|- ( A. z ( E. y e. A z e. y <-> z e. x ) <-> A. z ( z e. x <-> E. y e. A z e. y ) )
33	29 30 32	3bitri	|- ( U. A = x <-> A. z ( z e. x <-> E. y e. A z e. y ) )
34	27 33	sylib	|- ( ( ( A C_ On /\ x e. A ) /\ A. y e. A y C_ x ) -> A. z ( z e. x <-> E. y e. A z e. y ) )
35		notnotb	|- ( z e. x <-> -. -. z e. x )
36	35	bibi1i	|- ( ( z e. x <-> E. y e. A z e. y ) <-> ( -. -. z e. x <-> E. y e. A z e. y ) )
37		nbbn	|- ( ( -. -. z e. x <-> E. y e. A z e. y ) <-> -. ( -. z e. x <-> E. y e. A z e. y ) )
38	36 37	bitri	|- ( ( z e. x <-> E. y e. A z e. y ) <-> -. ( -. z e. x <-> E. y e. A z e. y ) )
39	38	albii	|- ( A. z ( z e. x <-> E. y e. A z e. y ) <-> A. z -. ( -. z e. x <-> E. y e. A z e. y ) )
40		alnex	|- ( A. z -. ( -. z e. x <-> E. y e. A z e. y ) <-> -. E. z ( -. z e. x <-> E. y e. A z e. y ) )
41	39 40	bitri	|- ( A. z ( z e. x <-> E. y e. A z e. y ) <-> -. E. z ( -. z e. x <-> E. y e. A z e. y ) )
42	34 41	sylib	|- ( ( ( A C_ On /\ x e. A ) /\ A. y e. A y C_ x ) -> -. E. z ( -. z e. x <-> E. y e. A z e. y ) )
43	42	ex	|- ( ( A C_ On /\ x e. A ) -> ( A. y e. A y C_ x -> -. E. z ( -. z e. x <-> E. y e. A z e. y ) ) )
44	21 43	sylbird	|- ( ( A C_ On /\ x e. A ) -> ( -. E. y e. A x e. y -> -. E. z ( -. z e. x <-> E. y e. A z e. y ) ) )
45	44	con4d	|- ( ( A C_ On /\ x e. A ) -> ( E. z ( -. z e. x <-> E. y e. A z e. y ) -> E. y e. A x e. y ) )
46	11 45	impbid2	|- ( ( A C_ On /\ x e. A ) -> ( E. y e. A x e. y <-> E. z ( -. z e. x <-> E. y e. A z e. y ) ) )
47	46	ralbidva	|- ( A C_ On -> ( A. x e. A E. y e. A x e. y <-> A. x e. A E. z ( -. z e. x <-> E. y e. A z e. y ) ) )
48		dminxp	|- ( dom ( _E i^i ( A X. A ) ) = A <-> A. x e. A E. y e. A x _E y )
49		epel	|- ( x _E y <-> x e. y )
50	49	rexbii	|- ( E. y e. A x _E y <-> E. y e. A x e. y )
51	50	ralbii	|- ( A. x e. A E. y e. A x _E y <-> A. x e. A E. y e. A x e. y )
52	48 51	bitri	|- ( dom ( _E i^i ( A X. A ) ) = A <-> A. x e. A E. y e. A x e. y )
53		ralnex	|- ( A. x e. A -. A. z ( z e. x <-> E. y e. A z e. y ) <-> -. E. x e. A A. z ( z e. x <-> E. y e. A z e. y ) )
54		exnal	|- ( E. z -. ( z e. x <-> E. y e. A z e. y ) <-> -. A. z ( z e. x <-> E. y e. A z e. y ) )
55		nbbn	|- ( ( -. z e. x <-> E. y e. A z e. y ) <-> -. ( z e. x <-> E. y e. A z e. y ) )
56	55	bicomi	|- ( -. ( z e. x <-> E. y e. A z e. y ) <-> ( -. z e. x <-> E. y e. A z e. y ) )
57	56	exbii	|- ( E. z -. ( z e. x <-> E. y e. A z e. y ) <-> E. z ( -. z e. x <-> E. y e. A z e. y ) )
58	54 57	bitr3i	|- ( -. A. z ( z e. x <-> E. y e. A z e. y ) <-> E. z ( -. z e. x <-> E. y e. A z e. y ) )
59	58	ralbii	|- ( A. x e. A -. A. z ( z e. x <-> E. y e. A z e. y ) <-> A. x e. A E. z ( -. z e. x <-> E. y e. A z e. y ) )
60	53 59	bitr3i	|- ( -. E. x e. A A. z ( z e. x <-> E. y e. A z e. y ) <-> A. x e. A E. z ( -. z e. x <-> E. y e. A z e. y ) )
61		uniel	|- ( U. A e. A <-> E. x e. A A. z ( z e. x <-> E. y e. A z e. y ) )
62	60 61	xchnxbir	|- ( -. U. A e. A <-> A. x e. A E. z ( -. z e. x <-> E. y e. A z e. y ) )
63	47 52 62	3bitr4g	|- ( A C_ On -> ( dom ( _E i^i ( A X. A ) ) = A <-> -. U. A e. A ) )