topmeet

Description: Two equivalent formulations of the meet of a collection of topologies. (Contributed by Jeff Hankins, 4-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	topmeet	$⊢ (X \in V \land S \subseteq TopOn (X)) \to 𝒫 X \cap ⋂ S = ⋃ \{k \in TopOn (X) \| \forall j \in S k \subseteq j\}$

Proof

Step	Hyp	Ref	Expression
1		topmtcl	$⊢ (X \in V \land S \subseteq TopOn (X)) \to 𝒫 X \cap ⋂ S \in TopOn (X)$
2		inss2	$⊢ 𝒫 X \cap ⋂ S \subseteq ⋂ S$
3		intss1	$⊢ j \in S \to ⋂ S \subseteq j$
4	2 3	sstrid	$⊢ j \in S \to 𝒫 X \cap ⋂ S \subseteq j$
5	4	rgen	$⊢ \forall j \in S 𝒫 X \cap ⋂ S \subseteq j$
6		sseq1	$⊢ k = 𝒫 X \cap ⋂ S \to (k \subseteq j \leftrightarrow 𝒫 X \cap ⋂ S \subseteq j)$
7	6	ralbidv	$⊢ k = 𝒫 X \cap ⋂ S \to (\forall j \in S k \subseteq j \leftrightarrow \forall j \in S 𝒫 X \cap ⋂ S \subseteq j)$
8	7	elrab	$⊢ 𝒫 X \cap ⋂ S \in \{k \in TopOn (X) \| \forall j \in S k \subseteq j\} \leftrightarrow (𝒫 X \cap ⋂ S \in TopOn (X) \land \forall j \in S 𝒫 X \cap ⋂ S \subseteq j)$
9	5 8	mpbiran2	$⊢ 𝒫 X \cap ⋂ S \in \{k \in TopOn (X) \| \forall j \in S k \subseteq j\} \leftrightarrow 𝒫 X \cap ⋂ S \in TopOn (X)$
10	1 9	sylibr	$⊢ (X \in V \land S \subseteq TopOn (X)) \to 𝒫 X \cap ⋂ S \in \{k \in TopOn (X) \| \forall j \in S k \subseteq j\}$
11		elssuni	$⊢ 𝒫 X \cap ⋂ S \in \{k \in TopOn (X) \| \forall j \in S k \subseteq j\} \to 𝒫 X \cap ⋂ S \subseteq ⋃ \{k \in TopOn (X) \| \forall j \in S k \subseteq j\}$
12	10 11	syl	$⊢ (X \in V \land S \subseteq TopOn (X)) \to 𝒫 X \cap ⋂ S \subseteq ⋃ \{k \in TopOn (X) \| \forall j \in S k \subseteq j\}$
13		toponuni	$⊢ k \in TopOn (X) \to X = ⋃ k$
14		eqimss2	$⊢ X = ⋃ k \to ⋃ k \subseteq X$
15	13 14	syl	$⊢ k \in TopOn (X) \to ⋃ k \subseteq X$
16		sspwuni	$⊢ k \subseteq 𝒫 X \leftrightarrow ⋃ k \subseteq X$
17	15 16	sylibr	$⊢ k \in TopOn (X) \to k \subseteq 𝒫 X$
18	17	3ad2ant2	$⊢ ((X \in V \land S \subseteq TopOn (X)) \land k \in TopOn (X) \land \forall j \in S k \subseteq j) \to k \subseteq 𝒫 X$
19		simp3	$⊢ ((X \in V \land S \subseteq TopOn (X)) \land k \in TopOn (X) \land \forall j \in S k \subseteq j) \to \forall j \in S k \subseteq j$
20		ssint	$⊢ k \subseteq ⋂ S \leftrightarrow \forall j \in S k \subseteq j$
21	19 20	sylibr	$⊢ ((X \in V \land S \subseteq TopOn (X)) \land k \in TopOn (X) \land \forall j \in S k \subseteq j) \to k \subseteq ⋂ S$
22	18 21	ssind	$⊢ ((X \in V \land S \subseteq TopOn (X)) \land k \in TopOn (X) \land \forall j \in S k \subseteq j) \to k \subseteq 𝒫 X \cap ⋂ S$
23		velpw	$⊢ k \in 𝒫 (𝒫 X \cap ⋂ S) \leftrightarrow k \subseteq 𝒫 X \cap ⋂ S$
24	22 23	sylibr	$⊢ ((X \in V \land S \subseteq TopOn (X)) \land k \in TopOn (X) \land \forall j \in S k \subseteq j) \to k \in 𝒫 (𝒫 X \cap ⋂ S)$
25	24	rabssdv	$⊢ (X \in V \land S \subseteq TopOn (X)) \to \{k \in TopOn (X) \| \forall j \in S k \subseteq j\} \subseteq 𝒫 (𝒫 X \cap ⋂ S)$
26		sspwuni	$⊢ \{k \in TopOn (X) \| \forall j \in S k \subseteq j\} \subseteq 𝒫 (𝒫 X \cap ⋂ S) \leftrightarrow ⋃ \{k \in TopOn (X) \| \forall j \in S k \subseteq j\} \subseteq 𝒫 X \cap ⋂ S$
27	25 26	sylib	$⊢ (X \in V \land S \subseteq TopOn (X)) \to ⋃ \{k \in TopOn (X) \| \forall j \in S k \subseteq j\} \subseteq 𝒫 X \cap ⋂ S$
28	12 27	eqssd	$⊢ (X \in V \land S \subseteq TopOn (X)) \to 𝒫 X \cap ⋂ S = ⋃ \{k \in TopOn (X) \| \forall j \in S k \subseteq j\}$

Metamath Proof Explorer

Theorem topmeet

Proof