intwun

Description: The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to A \subseteq WUni$
2	1	sselda	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land u \in A) \to u \in WUni$
3		wuntr	$⊢ u \in WUni \to Tr u$
4	2 3	syl	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land u \in A) \to Tr u$
5	4	ralrimiva	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to \forall u \in A Tr u$
6		trint	$⊢ \forall u \in A Tr u \to Tr ⋂ A$
7	5 6	syl	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to Tr ⋂ A$
8	2	wun0	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land u \in A) \to \emptyset \in u$
9	8	ralrimiva	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to \forall u \in A \emptyset \in u$
10		0ex	$⊢ \emptyset \in V$
11	10	elint2	$⊢ \emptyset \in ⋂ A \leftrightarrow \forall u \in A \emptyset \in u$
12	9 11	sylibr	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to \emptyset \in ⋂ A$
13	12	ne0d	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to ⋂ A \neq \emptyset$
14	2	adantlr	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land u \in A) \to u \in WUni$
15		intss1	$⊢ u \in A \to ⋂ A \subseteq u$
16	15	adantl	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land u \in A) \to ⋂ A \subseteq u$
17	16	sselda	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land u \in A) \land x \in ⋂ A) \to x \in u$
18	17	an32s	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land u \in A) \to x \in u$
19	14 18	wununi	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land u \in A) \to ⋃ x \in u$
20	19	ralrimiva	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \to \forall u \in A ⋃ x \in u$
21		vuniex	$⊢ ⋃ x \in V$
22	21	elint2	$⊢ ⋃ x \in ⋂ A \leftrightarrow \forall u \in A ⋃ x \in u$
23	20 22	sylibr	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \to ⋃ x \in ⋂ A$
24	14 18	wunpw	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land u \in A) \to 𝒫 x \in u$
25	24	ralrimiva	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \to \forall u \in A 𝒫 x \in u$
26		vpwex	$⊢ 𝒫 x \in V$
27	26	elint2	$⊢ 𝒫 x \in ⋂ A \leftrightarrow \forall u \in A 𝒫 x \in u$
28	25 27	sylibr	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \to 𝒫 x \in ⋂ A$
29	14	adantlr	$⊢ ((((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land y \in ⋂ A) \land u \in A) \to u \in WUni$
30	18	adantlr	$⊢ ((((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land y \in ⋂ A) \land u \in A) \to x \in u$
31	15	adantl	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land u \in A) \to ⋂ A \subseteq u$
32	31	sselda	$⊢ ((((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land u \in A) \land y \in ⋂ A) \to y \in u$
33	32	an32s	$⊢ ((((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land y \in ⋂ A) \land u \in A) \to y \in u$
34	29 30 33	wunpr	$⊢ ((((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land y \in ⋂ A) \land u \in A) \to \{x, y\} \in u$
35	34	ralrimiva	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land y \in ⋂ A) \to \forall u \in A \{x, y\} \in u$
36		prex	$⊢ \{x, y\} \in V$
37	36	elint2	$⊢ \{x, y\} \in ⋂ A \leftrightarrow \forall u \in A \{x, y\} \in u$
38	35 37	sylibr	$⊢ (((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \land y \in ⋂ A) \to \{x, y\} \in ⋂ A$
39	38	ralrimiva	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \to \forall y \in ⋂ A \{x, y\} \in ⋂ A$
40	23 28 39	3jca	$⊢ ((A \subseteq WUni \land A \neq \emptyset) \land x \in ⋂ A) \to (⋃ x \in ⋂ A \land 𝒫 x \in ⋂ A \land \forall y \in ⋂ A \{x, y\} \in ⋂ A)$
41	40	ralrimiva	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to \forall x \in ⋂ A (⋃ x \in ⋂ A \land 𝒫 x \in ⋂ A \land \forall y \in ⋂ A \{x, y\} \in ⋂ A)$
42		intex	$⊢ A \neq \emptyset \leftrightarrow ⋂ A \in V$
43	42	bilani	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to ⋂ A \in V$
44		iswun	$⊢ ⋂ A \in V \to (⋂ A \in WUni \leftrightarrow (Tr ⋂ A \land ⋂ A \neq \emptyset \land \forall x \in ⋂ A (⋃ x \in ⋂ A \land 𝒫 x \in ⋂ A \land \forall y \in ⋂ A \{x, y\} \in ⋂ A)))$
45	43 44	syl	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to (⋂ A \in WUni \leftrightarrow (Tr ⋂ A \land ⋂ A \neq \emptyset \land \forall x \in ⋂ A (⋃ x \in ⋂ A \land 𝒫 x \in ⋂ A \land \forall y \in ⋂ A \{x, y\} \in ⋂ A)))$
46	7 13 41 45	mpbir3and	$⊢ (A \subseteq WUni \land A \neq \emptyset) \to ⋂ A \in WUni$

Metamath Proof Explorer

Theorem intwun

Proof