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	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
2		ralnex	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
3	2	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
4		ssunib	⊢ ( 𝐴 ⊆ ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
5	4	notbii	⊢ ( ¬ 𝐴 ⊆ ∪ 𝐴 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
6	1 3 5	3bitr4ri	⊢ ( ¬ 𝐴 ⊆ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 )
7		simpll	⊢ ( ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ On )
8	7	sselda	⊢ ( ( ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
9		simpl	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → 𝐴 ⊆ On )
10	9	sselda	⊢ ( ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
11	10	adantr	⊢ ( ( ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ On )
12		ontri1	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
13	8 11 12	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
14	13	ralbidva	⊢ ( ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
15	14	rexbidva	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
16	6 15	bitr4id	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ¬ 𝐴 ⊆ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )
17		unielid	⊢ ( ∪ 𝐴 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 )
18	17	a1i	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ∪ 𝐴 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )
19	18	biimprd	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 → ∪ 𝐴 ∈ 𝐴 ) )
20	16 19	sylbid	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ¬ 𝐴 ⊆ ∪ 𝐴 → ∪ 𝐴 ∈ 𝐴 ) )
21	20	con1d	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ¬ ∪ 𝐴 ∈ 𝐴 → 𝐴 ⊆ ∪ 𝐴 ) )
22		uniss	⊢ ( 𝐴 ⊆ ∪ 𝐴 → ∪ 𝐴 ⊆ ∪ ∪ 𝐴 )
23	21 22	syl6	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 ⊆ ∪ ∪ 𝐴 ) )
24		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
25		orduniss	⊢ ( Ord ∪ 𝐴 → ∪ ∪ 𝐴 ⊆ ∪ 𝐴 )
26	24 25	syl	⊢ ( 𝐴 ⊆ On → ∪ ∪ 𝐴 ⊆ ∪ 𝐴 )
27	26	biantrud	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 ⊆ ∪ ∪ 𝐴 ↔ ( ∪ 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ⊆ ∪ 𝐴 ) ) )
28		eqss	⊢ ( ∪ 𝐴 = ∪ ∪ 𝐴 ↔ ( ∪ 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ⊆ ∪ 𝐴 ) )
29	27 28	bitr4di	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 ⊆ ∪ ∪ 𝐴 ↔ ∪ 𝐴 = ∪ ∪ 𝐴 ) )
30	29	adantr	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ∪ 𝐴 ⊆ ∪ ∪ 𝐴 ↔ ∪ 𝐴 = ∪ ∪ 𝐴 ) )
31	23 30	sylibd	⊢ ( ( 𝐴 ⊆ On ∧ ∪ 𝐴 ∈ On ) → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴 ) )
32	31	ex	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 ∈ On → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴 ) ) )
33		unon	⊢ ∪ On = On
34	33	a1i	⊢ ( ∪ 𝐴 = On → ∪ On = On )
35		unieq	⊢ ( ∪ 𝐴 = On → ∪ ∪ 𝐴 = ∪ On )
36		id	⊢ ( ∪ 𝐴 = On → ∪ 𝐴 = On )
37	34 35 36	3eqtr4rd	⊢ ( ∪ 𝐴 = On → ∪ 𝐴 = ∪ ∪ 𝐴 )
38	37	a1i13	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 = On → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴 ) ) )
39		ordeleqon	⊢ ( Ord ∪ 𝐴 ↔ ( ∪ 𝐴 ∈ On ∨ ∪ 𝐴 = On ) )
40	24 39	sylib	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 ∈ On ∨ ∪ 𝐴 = On ) )
41	32 38 40	mpjaod	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴 ) )