onintunirab

Description: The intersection of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 29-Jan-2025)

		Ref	Expression
	Assertion	onintunirab	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A = ⋃ \{x \in On \| \forall y \in A x \subseteq y\}$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in On \land \forall y \in A x \subseteq y) \to \forall y \in A x \subseteq y$
2		ssint	$⊢ x \subseteq ⋂ A \leftrightarrow \forall y \in A x \subseteq y$
3	1 2	sylibr	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in On \land \forall y \in A x \subseteq y) \to x \subseteq ⋂ A$
4		simp2	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in On \land \forall y \in A x \subseteq y) \to x \in On$
5		oninton	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in On$
6	5	3ad2ant1	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in On \land \forall y \in A x \subseteq y) \to ⋂ A \in On$
7		onsssuc	$⊢ (x \in On \land ⋂ A \in On) \to (x \subseteq ⋂ A \leftrightarrow x \in suc ⋂ A)$
8	4 6 7	syl2anc	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in On \land \forall y \in A x \subseteq y) \to (x \subseteq ⋂ A \leftrightarrow x \in suc ⋂ A)$
9	3 8	mpbid	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in On \land \forall y \in A x \subseteq y) \to x \in suc ⋂ A$
10	9	rabssdv	$⊢ (A \subseteq On \land A \neq \emptyset) \to \{x \in On \| \forall y \in A x \subseteq y\} \subseteq suc ⋂ A$
11		ssrab2	$⊢ \{x \in On \| \forall y \in A x \subseteq y\} \subseteq On$
12	11	a1i	$⊢ (A \subseteq On \land A \neq \emptyset) \to \{x \in On \| \forall y \in A x \subseteq y\} \subseteq On$
13		eloni	$⊢ ⋂ A \in On \to Ord ⋂ A$
14	5 13	syl	$⊢ (A \subseteq On \land A \neq \emptyset) \to Ord ⋂ A$
15		ordunisssuc	$⊢ (\{x \in On \| \forall y \in A x \subseteq y\} \subseteq On \land Ord ⋂ A) \to (⋃ \{x \in On \| \forall y \in A x \subseteq y\} \subseteq ⋂ A \leftrightarrow \{x \in On \| \forall y \in A x \subseteq y\} \subseteq suc ⋂ A)$
16	12 14 15	syl2anc	$⊢ (A \subseteq On \land A \neq \emptyset) \to (⋃ \{x \in On \| \forall y \in A x \subseteq y\} \subseteq ⋂ A \leftrightarrow \{x \in On \| \forall y \in A x \subseteq y\} \subseteq suc ⋂ A)$
17	10 16	mpbird	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋃ \{x \in On \| \forall y \in A x \subseteq y\} \subseteq ⋂ A$
18		sseq1	$⊢ x = ⋂ A \to (x \subseteq y \leftrightarrow ⋂ A \subseteq y)$
19	18	ralbidv	$⊢ x = ⋂ A \to (\forall y \in A x \subseteq y \leftrightarrow \forall y \in A ⋂ A \subseteq y)$
20		intss1	$⊢ y \in A \to ⋂ A \subseteq y$
21	20	rgen	$⊢ \forall y \in A ⋂ A \subseteq y$
22	21	a1i	$⊢ (A \subseteq On \land A \neq \emptyset) \to \forall y \in A ⋂ A \subseteq y$
23	19 5 22	elrabd	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in \{x \in On \| \forall y \in A x \subseteq y\}$
24		unissel	$⊢ (⋃ \{x \in On \| \forall y \in A x \subseteq y\} \subseteq ⋂ A \land ⋂ A \in \{x \in On \| \forall y \in A x \subseteq y\}) \to ⋃ \{x \in On \| \forall y \in A x \subseteq y\} = ⋂ A$
25	17 23 24	syl2anc	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋃ \{x \in On \| \forall y \in A x \subseteq y\} = ⋂ A$
26	25	eqcomd	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A = ⋃ \{x \in On \| \forall y \in A x \subseteq y\}$

Metamath Proof Explorer

Theorem onintunirab

Proof