onint

Description: The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of TakeutiZaring p. 45. (Contributed by NM, 31-Jan-1997)

		Ref	Expression
	Assertion	onint	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in A$

Proof

Step	Hyp	Ref	Expression
1		ordon	$⊢ Ord On$
2		tz7.5	$⊢ (Ord On \land A \subseteq On \land A \neq \emptyset) \to \exists x \in A A \cap x = \emptyset$
3	1 2	mp3an1	$⊢ (A \subseteq On \land A \neq \emptyset) \to \exists x \in A A \cap x = \emptyset$
4		ssel	$⊢ A \subseteq On \to (x \in A \to x \in On)$
5	4	imdistani	$⊢ (A \subseteq On \land x \in A) \to (A \subseteq On \land x \in On)$
6		ssel	$⊢ A \subseteq On \to (z \in A \to z \in On)$
7		ontri1	$⊢ (x \in On \land z \in On) \to (x \subseteq z \leftrightarrow \neg z \in x)$
8		ssel	$⊢ x \subseteq z \to (y \in x \to y \in z)$
9	7 8	syl6bir	$⊢ (x \in On \land z \in On) \to (\neg z \in x \to (y \in x \to y \in z))$
10	9	ex	$⊢ x \in On \to (z \in On \to (\neg z \in x \to (y \in x \to y \in z)))$
11	6 10	sylan9	$⊢ (A \subseteq On \land x \in On) \to (z \in A \to (\neg z \in x \to (y \in x \to y \in z)))$
12	11	com4r	$⊢ y \in x \to ((A \subseteq On \land x \in On) \to (z \in A \to (\neg z \in x \to y \in z)))$
13	12	imp31	$⊢ ((y \in x \land (A \subseteq On \land x \in On)) \land z \in A) \to (\neg z \in x \to y \in z)$
14	13	ralimdva	$⊢ (y \in x \land (A \subseteq On \land x \in On)) \to (\forall z \in A \neg z \in x \to \forall z \in A y \in z)$
15		disj	$⊢ A \cap x = \emptyset \leftrightarrow \forall z \in A \neg z \in x$
16		vex	$⊢ y \in V$
17	16	elint2	$⊢ y \in ⋂ A \leftrightarrow \forall z \in A y \in z$
18	14 15 17	3imtr4g	$⊢ (y \in x \land (A \subseteq On \land x \in On)) \to (A \cap x = \emptyset \to y \in ⋂ A)$
19	5 18	sylan2	$⊢ (y \in x \land (A \subseteq On \land x \in A)) \to (A \cap x = \emptyset \to y \in ⋂ A)$
20	19	exp32	$⊢ y \in x \to (A \subseteq On \to (x \in A \to (A \cap x = \emptyset \to y \in ⋂ A)))$
21	20	com4l	$⊢ A \subseteq On \to (x \in A \to (A \cap x = \emptyset \to (y \in x \to y \in ⋂ A)))$
22	21	imp32	$⊢ (A \subseteq On \land (x \in A \land A \cap x = \emptyset)) \to (y \in x \to y \in ⋂ A)$
23	22	ssrdv	$⊢ (A \subseteq On \land (x \in A \land A \cap x = \emptyset)) \to x \subseteq ⋂ A$
24		intss1	$⊢ x \in A \to ⋂ A \subseteq x$
25	24	ad2antrl	$⊢ (A \subseteq On \land (x \in A \land A \cap x = \emptyset)) \to ⋂ A \subseteq x$
26	23 25	eqssd	$⊢ (A \subseteq On \land (x \in A \land A \cap x = \emptyset)) \to x = ⋂ A$
27	26	eleq1d	$⊢ (A \subseteq On \land (x \in A \land A \cap x = \emptyset)) \to (x \in A \leftrightarrow ⋂ A \in A)$
28	27	biimpd	$⊢ (A \subseteq On \land (x \in A \land A \cap x = \emptyset)) \to (x \in A \to ⋂ A \in A)$
29	28	exp32	$⊢ A \subseteq On \to (x \in A \to (A \cap x = \emptyset \to (x \in A \to ⋂ A \in A)))$
30	29	com34	$⊢ A \subseteq On \to (x \in A \to (x \in A \to (A \cap x = \emptyset \to ⋂ A \in A)))$
31	30	pm2.43d	$⊢ A \subseteq On \to (x \in A \to (A \cap x = \emptyset \to ⋂ A \in A))$
32	31	rexlimdv	$⊢ A \subseteq On \to (\exists x \in A A \cap x = \emptyset \to ⋂ A \in A)$
33	3 32	syl5	$⊢ A \subseteq On \to ((A \subseteq On \land A \neq \emptyset) \to ⋂ A \in A)$
34	33	anabsi5	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in A$

Metamath Proof Explorer

Theorem onint

Proof