Theorem onmaxnelsup

Description: Two ways to say the maximum element of a class of ordinals is also the supremum of that class. (Contributed by RP, 27-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
2		ralnex	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
3	2	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
4		ssunib	⊢ ( 𝐴 ⊆ ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
5	4	notbii	⊢ ( ¬ 𝐴 ⊆ ∪ 𝐴 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
6	1 3 5	3bitr4ri	⊢ ( ¬ 𝐴 ⊆ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 )
7		simpl	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ On )
8	7	sselda	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
9		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
10	9	adantr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ On )
11		ontri1	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
12	8 10 11	syl2anc	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
13	12	ralbidva	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
14	13	rexbidva	⊢ ( 𝐴 ⊆ On → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ∈ 𝑦 ) )
15	6 14	bitr4id	⊢ ( 𝐴 ⊆ On → ( ¬ 𝐴 ⊆ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )