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	⊢ ( 𝐴 ⊆ On → ( dom ( E ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 ↔ ¬ ∪ 𝐴 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elirrv	⊢ ¬ 𝑥 ∈ 𝑥
2		pm5.501	⊢ ( ¬ 𝑥 ∈ 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ( ¬ 𝑥 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) ) )
3	1 2	mp1i	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ( ¬ 𝑥 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) ) )
4		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑥 ↔ 𝑥 ∈ 𝑥 ) )
5	4	notbid	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 ∈ 𝑥 ↔ ¬ 𝑥 ∈ 𝑥 ) )
6		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
7	6	rexbidv	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) )
8	5 7	bibi12d	⊢ ( 𝑧 = 𝑥 → ( ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ( ¬ 𝑥 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) ) )
9	3 8	bitr4d	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ) )
10	9	biimpd	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ) )
11	10	spimevw	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
12		ssel	⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On ) )
13	12	adantr	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On ) )
14	13	imp	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
15		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
16	15	adantr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ On )
17		ontri1	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
18	14 16 17	syl2anc	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
19	18	ralbidva	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
20		ralnex	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
21	19 20	bitrdi	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) )
22		unissb	⊢ ( ∪ 𝐴 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 )
23		simpr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ ∪ 𝐴 ⊆ 𝑥 ) → ∪ 𝐴 ⊆ 𝑥 )
24		elssuni	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴 )
25	24	ad2antlr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ ∪ 𝐴 ⊆ 𝑥 ) → 𝑥 ⊆ ∪ 𝐴 )
26	23 25	eqssd	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ ∪ 𝐴 ⊆ 𝑥 ) → ∪ 𝐴 = 𝑥 )
27	22 26	sylan2br	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) → ∪ 𝐴 = 𝑥 )
28		dfuni2	⊢ ∪ 𝐴 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 }
29	28	eqeq1i	⊢ ( ∪ 𝐴 = 𝑥 ↔ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 } = 𝑥 )
30		eqabcb	⊢ ( { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 } = 𝑥 ↔ ∀ 𝑧 ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥 ) )
31		bicom	⊢ ( ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
32	31	albii	⊢ ( ∀ 𝑧 ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
33	29 30 32	3bitri	⊢ ( ∪ 𝐴 = 𝑥 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
34	27 33	sylib	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
35		notnotb	⊢ ( 𝑧 ∈ 𝑥 ↔ ¬ ¬ 𝑧 ∈ 𝑥 )
36	35	bibi1i	⊢ ( ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ( ¬ ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
37		nbbn	⊢ ( ( ¬ ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ¬ ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
38	36 37	bitri	⊢ ( ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ¬ ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
39	38	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ¬ ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
40		alnex	⊢ ( ∀ 𝑧 ¬ ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ¬ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
41	39 40	bitri	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ¬ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
42	34 41	sylib	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) → ¬ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
43	42	ex	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 → ¬ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ) )
44	21 43	sylbird	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ) )
45	44	con4d	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) )
46	11 45	impbid2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ) )
47	46	ralbidva	⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ) )
48		dminxp	⊢ ( dom ( E ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 E 𝑦 )
49		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
50	49	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 E 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
51	50	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 E 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
52	48 51	bitri	⊢ ( dom ( E ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
53		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
54		exnal	⊢ ( ∃ 𝑧 ¬ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
55		nbbn	⊢ ( ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ¬ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
56	55	bicomi	⊢ ( ¬ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
57	56	exbii	⊢ ( ∃ 𝑧 ¬ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
58	54 57	bitr3i	⊢ ( ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
59	58	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
60	53 59	bitr3i	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
61		uniel	⊢ ( ∪ 𝐴 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
62	60 61	xchnxbir	⊢ ( ¬ ∪ 𝐴 ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ( ¬ 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ) )
63	47 52 62	3bitr4g	⊢ ( 𝐴 ⊆ On → ( dom ( E ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 ↔ ¬ ∪ 𝐴 ∈ 𝐴 ) )