fnemeet1

Description: The meet of a collection of equivalence classes of covers with respect to fineness. (Contributed by Jeff Hankins, 5-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	fnemeet1	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to (𝒫 X \cap ⋂_{t \in S} topGen (t)) Fne A$

Proof

Step	Hyp	Ref	Expression
1		unitg	$⊢ t \in S \to ⋃ topGen (t) = ⋃ t$
2	1	adantl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to ⋃ topGen (t) = ⋃ t$
3		unieq	$⊢ y = t \to ⋃ y = ⋃ t$
4	3	eqeq2d	$⊢ y = t \to (X = ⋃ y \leftrightarrow X = ⋃ t)$
5	4	rspccva	$⊢ (\forall y \in S X = ⋃ y \land t \in S) \to X = ⋃ t$
6	5	3ad2antl2	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to X = ⋃ t$
7	2 6	eqtr4d	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to ⋃ topGen (t) = X$
8		eqimss	$⊢ ⋃ topGen (t) = X \to ⋃ topGen (t) \subseteq X$
9	7 8	syl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to ⋃ topGen (t) \subseteq X$
10		sspwuni	$⊢ topGen (t) \subseteq 𝒫 X \leftrightarrow ⋃ topGen (t) \subseteq X$
11	9 10	sylibr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to topGen (t) \subseteq 𝒫 X$
12	11	ralrimiva	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to \forall t \in S topGen (t) \subseteq 𝒫 X$
13		ne0i	$⊢ A \in S \to S \neq \emptyset$
14	13	3ad2ant3	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to S \neq \emptyset$
15		riinn0	$⊢ (\forall t \in S topGen (t) \subseteq 𝒫 X \land S \neq \emptyset) \to 𝒫 X \cap ⋂_{t \in S} topGen (t) = ⋂_{t \in S} topGen (t)$
16	12 14 15	syl2anc	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to 𝒫 X \cap ⋂_{t \in S} topGen (t) = ⋂_{t \in S} topGen (t)$
17		simp3	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to A \in S$
18		ssid	$⊢ topGen (A) \subseteq topGen (A)$
19		fveq2	$⊢ t = A \to topGen (t) = topGen (A)$
20	19	sseq1d	$⊢ t = A \to (topGen (t) \subseteq topGen (A) \leftrightarrow topGen (A) \subseteq topGen (A))$
21	20	rspcev	$⊢ (A \in S \land topGen (A) \subseteq topGen (A)) \to \exists t \in S topGen (t) \subseteq topGen (A)$
22	17 18 21	sylancl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to \exists t \in S topGen (t) \subseteq topGen (A)$
23		iinss	$⊢ \exists t \in S topGen (t) \subseteq topGen (A) \to ⋂_{t \in S} topGen (t) \subseteq topGen (A)$
24	22 23	syl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋂_{t \in S} topGen (t) \subseteq topGen (A)$
25	24	unissd	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋃ ⋂_{t \in S} topGen (t) \subseteq ⋃ topGen (A)$
26		unitg	$⊢ A \in S \to ⋃ topGen (A) = ⋃ A$
27	26	3ad2ant3	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋃ topGen (A) = ⋃ A$
28	25 27	sseqtrd	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋃ ⋂_{t \in S} topGen (t) \subseteq ⋃ A$
29		unieq	$⊢ y = A \to ⋃ y = ⋃ A$
30	29	eqeq2d	$⊢ y = A \to (X = ⋃ y \leftrightarrow X = ⋃ A)$
31	30	rspccva	$⊢ (\forall y \in S X = ⋃ y \land A \in S) \to X = ⋃ A$
32	31	3adant1	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to X = ⋃ A$
33	32	adantr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to X = ⋃ A$
34	33 6	eqtr3d	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to ⋃ A = ⋃ t$
35		simpr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to t \in S$
36		ssid	$⊢ t \subseteq t$
37		eltg3i	$⊢ (t \in S \land t \subseteq t) \to ⋃ t \in topGen (t)$
38	35 36 37	sylancl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to ⋃ t \in topGen (t)$
39	34 38	eqeltrd	$⊢ ((X \in V \land \forall y \in S X = ⋃ y \land A \in S) \land t \in S) \to ⋃ A \in topGen (t)$
40	39	ralrimiva	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to \forall t \in S ⋃ A \in topGen (t)$
41		uniexg	$⊢ A \in S \to ⋃ A \in V$
42	41	3ad2ant3	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋃ A \in V$
43		eliin	$⊢ ⋃ A \in V \to (⋃ A \in ⋂_{t \in S} topGen (t) \leftrightarrow \forall t \in S ⋃ A \in topGen (t))$
44	42 43	syl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to (⋃ A \in ⋂_{t \in S} topGen (t) \leftrightarrow \forall t \in S ⋃ A \in topGen (t))$
45	40 44	mpbird	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋃ A \in ⋂_{t \in S} topGen (t)$
46		elssuni	$⊢ ⋃ A \in ⋂_{t \in S} topGen (t) \to ⋃ A \subseteq ⋃ ⋂_{t \in S} topGen (t)$
47	45 46	syl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋃ A \subseteq ⋃ ⋂_{t \in S} topGen (t)$
48	28 47	eqssd	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋃ ⋂_{t \in S} topGen (t) = ⋃ A$
49		eqid	$⊢ ⋃ ⋂_{t \in S} topGen (t) = ⋃ ⋂_{t \in S} topGen (t)$
50		eqid	$⊢ ⋃ A = ⋃ A$
51	49 50	isfne4	$⊢ ⋂_{t \in S} topGen (t) Fne A \leftrightarrow (⋃ ⋂_{t \in S} topGen (t) = ⋃ A \land ⋂_{t \in S} topGen (t) \subseteq topGen (A))$
52	48 24 51	sylanbrc	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to ⋂_{t \in S} topGen (t) Fne A$
53	16 52	eqbrtrd	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land A \in S) \to (𝒫 X \cap ⋂_{t \in S} topGen (t)) Fne A$

Metamath Proof Explorer

Theorem fnemeet1

Proof