Theorem onsupeqnmax

Description: Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupeqnmax	⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ( ∪ 𝐴 = ∪ ∪ 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ On )
2	1	sselda	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
3		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
4	3	adantr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ On )
5		ontri1	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
6	2 4 5	syl2anc	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
7	6	ralbidva	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
8	7	rexbidva	⊢ ( 𝐴 ⊆ On → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
9	8	notbid	⊢ ( 𝐴 ⊆ On → ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
10	9	bicomd	⊢ ( 𝐴 ⊆ On → ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )
11		dfrex2	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 )
12	11	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 )
13		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 )
14	12 13	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 )
15		unielid	⊢ ( ∪ 𝐴 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 )
16	15	notbii	⊢ ( ¬ ∪ 𝐴 ∈ 𝐴 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 )
17	10 14 16	3bitr4g	⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∪ 𝐴 ∈ 𝐴 ) )
18		onsupnmax	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴 ) )
19	18	pm4.71rd	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 ∈ 𝐴 ↔ ( ∪ 𝐴 = ∪ ∪ 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ) )
20	17 19	bitrd	⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ( ∪ 𝐴 = ∪ ∪ 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ) )