fnemeet2

Description: The meet of equivalence classes under the fineness relation-part two. (Contributed by Jeff Hankins, 6-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		riin0	$⊢ S = \emptyset \to 𝒫 X \cap ⋂_{t \in S} topGen (t) = 𝒫 X$
2	1	unieqd	$⊢ S = \emptyset \to ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)) = ⋃ 𝒫 X$
3		unipw	$⊢ ⋃ 𝒫 X = X$
4	2 3	eqtr2di	$⊢ S = \emptyset \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
5	4	a1i	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (S = \emptyset \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)))$
6		n0	$⊢ S \neq \emptyset \leftrightarrow \exists x x \in S$
7		unieq	$⊢ y = x \to ⋃ y = ⋃ x$
8	7	eqeq2d	$⊢ y = x \to (X = ⋃ y \leftrightarrow X = ⋃ x)$
9	8	rspccva	$⊢ (\forall y \in S X = ⋃ y \land x \in S) \to X = ⋃ x$
10	9	3adant1	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to X = ⋃ x$
11		fnemeet1	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to (𝒫 X \cap ⋂_{t \in S} topGen (t)) Fne x$
12		eqid	$⊢ ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)) = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
13		eqid	$⊢ ⋃ x = ⋃ x$
14	12 13	fnebas	$⊢ (𝒫 X \cap ⋂_{t \in S} topGen (t)) Fne x \to ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)) = ⋃ x$
15	11 14	syl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)) = ⋃ x$
16	10 15	eqtr4d	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
17	16	3expia	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (x \in S \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)))$
18	17	exlimdv	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (\exists x x \in S \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)))$
19	6 18	syl5bi	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (S \neq \emptyset \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)))$
20	5 19	pm2.61dne	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
21	20	adantr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t))) \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
22		eqid	$⊢ ⋃ T = ⋃ T$
23	22 12	fnebas	$⊢ T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \to ⋃ T = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
24	23	adantl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t))) \to ⋃ T = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
25	21 24	eqtr4d	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t))) \to X = ⋃ T$
26	25	ex	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \to X = ⋃ T)$
27		fnetr	$⊢ (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \land (𝒫 X \cap ⋂_{t \in S} topGen (t)) Fne x) \to T Fne x$
28	27	expcom	$⊢ (𝒫 X \cap ⋂_{t \in S} topGen (t)) Fne x \to (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \to T Fne x)$
29	11 28	syl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \to T Fne x)$
30	29	3expa	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land x \in S) \to (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \to T Fne x)$
31	30	ralrimdva	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \to \forall x \in S T Fne x)$
32	26 31	jcad	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \to (X = ⋃ T \land \forall x \in S T Fne x))$
33		simprl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to X = ⋃ T$
34	20	adantr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to X = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
35	33 34	eqtr3d	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to ⋃ T = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t))$
36		eqimss2	$⊢ X = ⋃ T \to ⋃ T \subseteq X$
37	36	ad2antrl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to ⋃ T \subseteq X$
38		sspwuni	$⊢ T \subseteq 𝒫 X \leftrightarrow ⋃ T \subseteq X$
39	37 38	sylibr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to T \subseteq 𝒫 X$
40		breq2	$⊢ x = t \to (T Fne x \leftrightarrow T Fne t)$
41	40	cbvralvw	$⊢ \forall x \in S T Fne x \leftrightarrow \forall t \in S T Fne t$
42		fnetg	$⊢ T Fne t \to T \subseteq topGen (t)$
43	42	ralimi	$⊢ \forall t \in S T Fne t \to \forall t \in S T \subseteq topGen (t)$
44	41 43	sylbi	$⊢ \forall x \in S T Fne x \to \forall t \in S T \subseteq topGen (t)$
45	44	ad2antll	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to \forall t \in S T \subseteq topGen (t)$
46		ssiin	$⊢ T \subseteq ⋂_{t \in S} topGen (t) \leftrightarrow \forall t \in S T \subseteq topGen (t)$
47	45 46	sylibr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to T \subseteq ⋂_{t \in S} topGen (t)$
48	39 47	ssind	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to T \subseteq 𝒫 X \cap ⋂_{t \in S} topGen (t)$
49		pwexg	$⊢ X \in V \to 𝒫 X \in V$
50		inex1g	$⊢ 𝒫 X \in V \to 𝒫 X \cap ⋂_{t \in S} topGen (t) \in V$
51	49 50	syl	$⊢ X \in V \to 𝒫 X \cap ⋂_{t \in S} topGen (t) \in V$
52	51	ad2antrr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to 𝒫 X \cap ⋂_{t \in S} topGen (t) \in V$
53		bastg	$⊢ 𝒫 X \cap ⋂_{t \in S} topGen (t) \in V \to 𝒫 X \cap ⋂_{t \in S} topGen (t) \subseteq topGen (𝒫 X \cap ⋂_{t \in S} topGen (t))$
54	52 53	syl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to 𝒫 X \cap ⋂_{t \in S} topGen (t) \subseteq topGen (𝒫 X \cap ⋂_{t \in S} topGen (t))$
55	48 54	sstrd	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to T \subseteq topGen (𝒫 X \cap ⋂_{t \in S} topGen (t))$
56	22 12	isfne4	$⊢ T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \leftrightarrow (⋃ T = ⋃ (𝒫 X \cap ⋂_{t \in S} topGen (t)) \land T \subseteq topGen (𝒫 X \cap ⋂_{t \in S} topGen (t)))$
57	35 55 56	sylanbrc	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S T Fne x)) \to T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t))$
58	57	ex	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to ((X = ⋃ T \land \forall x \in S T Fne x) \to T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)))$
59	32 58	impbid	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (T Fne (𝒫 X \cap ⋂_{t \in S} topGen (t)) \leftrightarrow (X = ⋃ T \land \forall x \in S T Fne x))$

Metamath Proof Explorer

Theorem fnemeet2

Proof