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	$⊢ A \subseteq On \to (\neg A \subseteq ⋃ A \leftrightarrow \exists x \in A \forall y \in A y \subseteq x)$

Step	Hyp	Ref	Expression
1		rexnal	$⊢ \exists x \in A \neg \exists y \in A x \in y \leftrightarrow \neg \forall x \in A \exists y \in A x \in y$
2		ralnex	$⊢ \forall y \in A \neg x \in y \leftrightarrow \neg \exists y \in A x \in y$
3	2	rexbii	$⊢ \exists x \in A \forall y \in A \neg x \in y \leftrightarrow \exists x \in A \neg \exists y \in A x \in y$
4		ssunib	$⊢ A \subseteq ⋃ A \leftrightarrow \forall x \in A \exists y \in A x \in y$
5	4	notbii	$⊢ \neg A \subseteq ⋃ A \leftrightarrow \neg \forall x \in A \exists y \in A x \in y$
6	1 3 5	3bitr4ri	$⊢ \neg A \subseteq ⋃ A \leftrightarrow \exists x \in A \forall y \in A \neg x \in y$
7		simpl	$⊢ (A \subseteq On \land x \in A) \to A \subseteq On$
8	7	sselda	$⊢ ((A \subseteq On \land x \in A) \land y \in A) \to y \in On$
9		ssel2	$⊢ (A \subseteq On \land x \in A) \to x \in On$
10	9	adantr	$⊢ ((A \subseteq On \land x \in A) \land y \in A) \to x \in On$
11		ontri1	$⊢ (y \in On \land x \in On) \to (y \subseteq x \leftrightarrow \neg x \in y)$
12	8 10 11	syl2anc	$⊢ ((A \subseteq On \land x \in A) \land y \in A) \to (y \subseteq x \leftrightarrow \neg x \in y)$
13	12	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)$
14	13	rexbidva	$⊢ A \subseteq On \to (\exists x \in A \forall y \in A y \subseteq x \leftrightarrow \exists x \in A \forall y \in A \neg x \in y)$
15	6 14	bitr4id	$⊢ A \subseteq On \to (\neg A \subseteq ⋃ A \leftrightarrow \exists x \in A \forall y \in A y \subseteq x)$

Metamath Proof Explorer