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 \subseteq On \to (dom (E \cap (A \times A)) = A \leftrightarrow \neg ⋃ A \in A)$

Proof

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

Metamath Proof Explorer

Theorem onsupmaxb

Proof