fnejoin2

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

		Ref	Expression
	Assertion	fnejoin2	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \leftrightarrow (X = ⋃ T \land \forall x \in S x Fne T))$

Proof

Step	Hyp	Ref	Expression
1		unisng	$⊢ X \in V \to ⋃ \{X\} = X$
2	1	eqcomd	$⊢ X \in V \to X = ⋃ \{X\}$
3	2	adantr	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to X = ⋃ \{X\}$
4		iftrue	$⊢ S = \emptyset \to if (S = \emptyset, \{X\}, ⋃ S) = \{X\}$
5	4	unieqd	$⊢ S = \emptyset \to ⋃ if (S = \emptyset, \{X\}, ⋃ S) = ⋃ \{X\}$
6	5	eqeq2d	$⊢ S = \emptyset \to (X = ⋃ if (S = \emptyset, \{X\}, ⋃ S) \leftrightarrow X = ⋃ \{X\})$
7	3 6	syl5ibrcom	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (S = \emptyset \to X = ⋃ if (S = \emptyset, \{X\}, ⋃ S))$
8		n0	$⊢ S \neq \emptyset \leftrightarrow \exists x x \in S$
9		unieq	$⊢ y = x \to ⋃ y = ⋃ x$
10	9	eqeq2d	$⊢ y = x \to (X = ⋃ y \leftrightarrow X = ⋃ x)$
11	10	rspccva	$⊢ (\forall y \in S X = ⋃ y \land x \in S) \to X = ⋃ x$
12	11	3adant1	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to X = ⋃ x$
13		fnejoin1	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to x Fne if (S = \emptyset, \{X\}, ⋃ S)$
14		eqid	$⊢ ⋃ x = ⋃ x$
15		eqid	$⊢ ⋃ if (S = \emptyset, \{X\}, ⋃ S) = ⋃ if (S = \emptyset, \{X\}, ⋃ S)$
16	14 15	fnebas	$⊢ x Fne if (S = \emptyset, \{X\}, ⋃ S) \to ⋃ x = ⋃ if (S = \emptyset, \{X\}, ⋃ S)$
17	13 16	syl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to ⋃ x = ⋃ if (S = \emptyset, \{X\}, ⋃ S)$
18	12 17	eqtrd	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to X = ⋃ if (S = \emptyset, \{X\}, ⋃ S)$
19	18	3expia	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (x \in S \to X = ⋃ if (S = \emptyset, \{X\}, ⋃ S))$
20	19	exlimdv	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (\exists x x \in S \to X = ⋃ if (S = \emptyset, \{X\}, ⋃ S))$
21	8 20	syl5bi	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (S \neq \emptyset \to X = ⋃ if (S = \emptyset, \{X\}, ⋃ S))$
22	7 21	pm2.61dne	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to X = ⋃ if (S = \emptyset, \{X\}, ⋃ S)$
23		eqid	$⊢ ⋃ T = ⋃ T$
24	15 23	fnebas	$⊢ if (S = \emptyset, \{X\}, ⋃ S) Fne T \to ⋃ if (S = \emptyset, \{X\}, ⋃ S) = ⋃ T$
25	22 24	sylan9eq	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land if (S = \emptyset, \{X\}, ⋃ S) Fne T) \to X = ⋃ T$
26	25	ex	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \to X = ⋃ T)$
27		fnetr	$⊢ (x Fne if (S = \emptyset, \{X\}, ⋃ S) \land if (S = \emptyset, \{X\}, ⋃ S) Fne T) \to x Fne T$
28	27	ex	$⊢ x Fne if (S = \emptyset, \{X\}, ⋃ S) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \to x Fne T)$
29	13 28	syl	$⊢ (X \in V \land \forall y \in S X = ⋃ y \land x \in S) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \to x Fne T)$
30	29	3expa	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land x \in S) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \to x Fne T)$
31	30	ralrimdva	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \to \forall x \in S x Fne T)$
32	26 31	jcad	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \to (X = ⋃ T \land \forall x \in S x Fne T))$
33	22	adantr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to X = ⋃ if (S = \emptyset, \{X\}, ⋃ S)$
34		simprl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to X = ⋃ T$
35	33 34	eqtr3d	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to ⋃ if (S = \emptyset, \{X\}, ⋃ S) = ⋃ T$
36		sseq1	$⊢ \{X\} = if (S = \emptyset, \{X\}, ⋃ S) \to (\{X\} \subseteq topGen (T) \leftrightarrow if (S = \emptyset, \{X\}, ⋃ S) \subseteq topGen (T))$
37		sseq1	$⊢ ⋃ S = if (S = \emptyset, \{X\}, ⋃ S) \to (⋃ S \subseteq topGen (T) \leftrightarrow if (S = \emptyset, \{X\}, ⋃ S) \subseteq topGen (T))$
38		elex	$⊢ X \in V \to X \in V$
39	38	ad2antrr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to X \in V$
40	34 39	eqeltrrd	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to ⋃ T \in V$
41		uniexb	$⊢ T \in V \leftrightarrow ⋃ T \in V$
42	40 41	sylibr	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to T \in V$
43		ssid	$⊢ T \subseteq T$
44		eltg3i	$⊢ (T \in V \land T \subseteq T) \to ⋃ T \in topGen (T)$
45	42 43 44	sylancl	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to ⋃ T \in topGen (T)$
46	34 45	eqeltrd	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to X \in topGen (T)$
47	46	snssd	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to \{X\} \subseteq topGen (T)$
48	47	adantr	$⊢ (((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \land S = \emptyset) \to \{X\} \subseteq topGen (T)$
49		simplrr	$⊢ (((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \land \neg S = \emptyset) \to \forall x \in S x Fne T$
50		fnetg	$⊢ x Fne T \to x \subseteq topGen (T)$
51	50	ralimi	$⊢ \forall x \in S x Fne T \to \forall x \in S x \subseteq topGen (T)$
52	49 51	syl	$⊢ (((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \land \neg S = \emptyset) \to \forall x \in S x \subseteq topGen (T)$
53		unissb	$⊢ ⋃ S \subseteq topGen (T) \leftrightarrow \forall x \in S x \subseteq topGen (T)$
54	52 53	sylibr	$⊢ (((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \land \neg S = \emptyset) \to ⋃ S \subseteq topGen (T)$
55	36 37 48 54	ifbothda	$⊢ ((X \in V \land \forall y \in S X = ⋃ y) \land (X = ⋃ T \land \forall x \in S x Fne T)) \to if (S = \emptyset, \{X\}, ⋃ S) \subseteq topGen (T)$
56	15 23	isfne4	$⊢ if (S = \emptyset, \{X\}, ⋃ S) Fne T \leftrightarrow (⋃ if (S = \emptyset, \{X\}, ⋃ S) = ⋃ T \land if (S = \emptyset, \{X\}, ⋃ S) \subseteq 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 x Fne T)) \to if (S = \emptyset, \{X\}, ⋃ S) Fne T$
58	57	ex	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to ((X = ⋃ T \land \forall x \in S x Fne T) \to if (S = \emptyset, \{X\}, ⋃ S) Fne T)$
59	32 58	impbid	$⊢ (X \in V \land \forall y \in S X = ⋃ y) \to (if (S = \emptyset, \{X\}, ⋃ S) Fne T \leftrightarrow (X = ⋃ T \land \forall x \in S x Fne T))$

Metamath Proof Explorer

Theorem fnejoin2

Proof