iunconnlem2

	Ref	Expression
Hypotheses	iunconnlem2.1	$⊢ ψ \leftrightarrow ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v)$
	iunconnlem2.2	$⊢ φ \to J \in TopOn (X)$
	iunconnlem2.3	$⊢ (φ \land k \in A) \to B \subseteq X$
	iunconnlem2.4	$⊢ (φ \land k \in A) \to P \in B$
	iunconnlem2.5	$⊢ (φ \land k \in A) \to J ↾_{𝑡} B \in Conn$
Assertion	iunconnlem2	$⊢ φ \to J ↾_{𝑡} ⋃_{k \in A} B \in Conn$

Proof

Step	Hyp	Ref	Expression
1		iunconnlem2.1	$⊢ ψ \leftrightarrow ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v)$
2		iunconnlem2.2	$⊢ φ \to J \in TopOn (X)$
3		iunconnlem2.3	$⊢ (φ \land k \in A) \to B \subseteq X$
4		iunconnlem2.4	$⊢ (φ \land k \in A) \to P \in B$
5		iunconnlem2.5	$⊢ (φ \land k \in A) \to J ↾_{𝑡} B \in Conn$
6	3	ex	$⊢ φ \to (k \in A \to B \subseteq X)$
7	6	ralrimiv	$⊢ φ \to \forall k \in A B \subseteq X$
8		iunss	$⊢ ⋃_{k \in A} B \subseteq X \leftrightarrow \forall k \in A B \subseteq X$
9	8	biimpri	$⊢ \forall k \in A B \subseteq X \to ⋃_{k \in A} B \subseteq X$
10	7 9	syl	$⊢ φ \to ⋃_{k \in A} B \subseteq X$
11	1	biimpi	$⊢ ψ \to ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v)$
12	11	simprd	$⊢ ψ \to ⋃_{k \in A} B \subseteq u \cup v$
13		simp-4r	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to u \cap ⋃_{k \in A} B \neq \emptyset$
14	11 13	syl	$⊢ ψ \to u \cap ⋃_{k \in A} B \neq \emptyset$
15		n0	$⊢ u \cap ⋃_{k \in A} B \neq \emptyset \leftrightarrow \exists w w \in (u \cap ⋃_{k \in A} B)$
16	15	biimpi	$⊢ u \cap ⋃_{k \in A} B \neq \emptyset \to \exists w w \in (u \cap ⋃_{k \in A} B)$
17	14 16	syl	$⊢ ψ \to \exists w w \in (u \cap ⋃_{k \in A} B)$
18		inss2	$⊢ u \cap ⋃_{k \in A} B \subseteq ⋃_{k \in A} B$
19		id	$⊢ w \in (u \cap ⋃_{k \in A} B) \to w \in (u \cap ⋃_{k \in A} B)$
20	18 19	sselid	$⊢ w \in (u \cap ⋃_{k \in A} B) \to w \in ⋃_{k \in A} B$
21		eliun	$⊢ w \in ⋃_{k \in A} B \leftrightarrow \exists k \in A w \in B$
22	21	biimpi	$⊢ w \in ⋃_{k \in A} B \to \exists k \in A w \in B$
23	20 22	syl	$⊢ w \in (u \cap ⋃_{k \in A} B) \to \exists k \in A w \in B$
24		rexn0	$⊢ \exists k \in A w \in B \to A \neq \emptyset$
25	23 24	syl	$⊢ w \in (u \cap ⋃_{k \in A} B) \to A \neq \emptyset$
26	25	exlimiv	$⊢ \exists w w \in (u \cap ⋃_{k \in A} B) \to A \neq \emptyset$
27	17 26	syl	$⊢ ψ \to A \neq \emptyset$
28		nfv	$⊢ Ⅎ k (φ \land u \in J)$
29		nfv	$⊢ Ⅎ k v \in J$
30	28 29	nfan	$⊢ Ⅎ k ((φ \land u \in J) \land v \in J)$
31		nfcv	$⊢ \underline{Ⅎ} k u$
32		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k \in A} B$
33	31 32	nfin	$⊢ \underline{Ⅎ} k (u \cap ⋃_{k \in A} B)$
34		nfcv	$⊢ \underline{Ⅎ} k \emptyset$
35	33 34	nfne	$⊢ Ⅎ k u \cap ⋃_{k \in A} B \neq \emptyset$
36	30 35	nfan	$⊢ Ⅎ k (((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset)$
37		nfcv	$⊢ \underline{Ⅎ} k v$
38	37 32	nfin	$⊢ \underline{Ⅎ} k (v \cap ⋃_{k \in A} B)$
39	38 34	nfne	$⊢ Ⅎ k v \cap ⋃_{k \in A} B \neq \emptyset$
40	36 39	nfan	$⊢ Ⅎ k ((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset)$
41		nfcv	$⊢ \underline{Ⅎ} k (u \cap v)$
42		nfcv	$⊢ \underline{Ⅎ} k X$
43	42 32	nfdif	$⊢ \underline{Ⅎ} k (X ∖ ⋃_{k \in A} B)$
44	41 43	nfss	$⊢ Ⅎ k u \cap v \subseteq X ∖ ⋃_{k \in A} B$
45	40 44	nfan	$⊢ Ⅎ k (((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)$
46		nfcv	$⊢ \underline{Ⅎ} k (u \cup v)$
47	32 46	nfss	$⊢ Ⅎ k ⋃_{k \in A} B \subseteq u \cup v$
48	45 47	nfan	$⊢ Ⅎ k ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v)$
49	1	nfbii	$⊢ Ⅎ k ψ \leftrightarrow Ⅎ k ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v)$
50	48 49	mpbir	$⊢ Ⅎ k ψ$
51		simp-6l	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to φ$
52	11 51	syl	$⊢ ψ \to φ$
53	52 4	sylan	$⊢ (ψ \land k \in A) \to P \in B$
54	53	ex	$⊢ ψ \to (k \in A \to P \in B)$
55	50 54	ralrimi	$⊢ ψ \to \forall k \in A P \in B$
56		r19.2z	$⊢ (A \neq \emptyset \land \forall k \in A P \in B) \to \exists k \in A P \in B$
57	56	ancoms	$⊢ (\forall k \in A P \in B \land A \neq \emptyset) \to \exists k \in A P \in B$
58	57	ancoms	$⊢ (A \neq \emptyset \land \forall k \in A P \in B) \to \exists k \in A P \in B$
59	27 55 58	syl2anc	$⊢ ψ \to \exists k \in A P \in B$
60		eliun	$⊢ P \in ⋃_{k \in A} B \leftrightarrow \exists k \in A P \in B$
61	60	biimpri	$⊢ \exists k \in A P \in B \to P \in ⋃_{k \in A} B$
62	59 61	syl	$⊢ ψ \to P \in ⋃_{k \in A} B$
63	12 62	sseldd	$⊢ ψ \to P \in (u \cup v)$
64		elun	$⊢ P \in (u \cup v) \leftrightarrow (P \in u \lor P \in v)$
65	64	biimpi	$⊢ P \in (u \cup v) \to (P \in u \lor P \in v)$
66	63 65	syl	$⊢ ψ \to (P \in u \lor P \in v)$
67	1 66	sylbir	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to (P \in u \lor P \in v)$
68	52 2	syl	$⊢ ψ \to J \in TopOn (X)$
69	52 3	sylan	$⊢ (ψ \land k \in A) \to B \subseteq X$
70	52 5	sylan	$⊢ (ψ \land k \in A) \to J ↾_{𝑡} B \in Conn$
71		simp-6r	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to u \in J$
72	11 71	syl	$⊢ ψ \to u \in J$
73		simp-5r	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to v \in J$
74	11 73	syl	$⊢ ψ \to v \in J$
75		simpllr	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to v \cap ⋃_{k \in A} B \neq \emptyset$
76	11 75	syl	$⊢ ψ \to v \cap ⋃_{k \in A} B \neq \emptyset$
77		simplr	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to u \cap v \subseteq X ∖ ⋃_{k \in A} B$
78	11 77	syl	$⊢ ψ \to u \cap v \subseteq X ∖ ⋃_{k \in A} B$
79	68 69 53 70 72 74 76 78 12 50	iunconnlem	$⊢ ψ \to \neg P \in u$
80		incom	$⊢ v \cap u = u \cap v$
81	80 78	eqsstrid	$⊢ ψ \to v \cap u \subseteq X ∖ ⋃_{k \in A} B$
82		uncom	$⊢ v \cup u = u \cup v$
83	12 82	sseqtrrdi	$⊢ ψ \to ⋃_{k \in A} B \subseteq v \cup u$
84	68 69 53 70 74 72 14 81 83 50	iunconnlem	$⊢ ψ \to \neg P \in v$
85		pm4.56	$⊢ (\neg P \in u \land \neg P \in v) \leftrightarrow \neg (P \in u \lor P \in v)$
86	85	biimpi	$⊢ (\neg P \in u \land \neg P \in v) \to \neg (P \in u \lor P \in v)$
87	86	idiALT	$⊢ (\neg P \in u \land \neg P \in v) \to \neg (P \in u \lor P \in v)$
88	79 84 87	syl2anc	$⊢ ψ \to \neg (P \in u \lor P \in v)$
89	1 88	sylbir	$⊢ ((((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \land ⋃_{k \in A} B \subseteq u \cup v) \to \neg (P \in u \lor P \in v)$
90	67 89	pm2.65da	$⊢ (((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v$
91	90	ex	$⊢ ((((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \land v \cap ⋃_{k \in A} B \neq \emptyset) \to (u \cap v \subseteq X ∖ ⋃_{k \in A} B \to \neg ⋃_{k \in A} B \subseteq u \cup v)$
92	91	ex	$⊢ (((φ \land u \in J) \land v \in J) \land u \cap ⋃_{k \in A} B \neq \emptyset) \to (v \cap ⋃_{k \in A} B \neq \emptyset \to (u \cap v \subseteq X ∖ ⋃_{k \in A} B \to \neg ⋃_{k \in A} B \subseteq u \cup v))$
93	92	ex3	$⊢ (φ \land u \in J \land v \in J) \to (u \cap ⋃_{k \in A} B \neq \emptyset \to (v \cap ⋃_{k \in A} B \neq \emptyset \to (u \cap v \subseteq X ∖ ⋃_{k \in A} B \to \neg ⋃_{k \in A} B \subseteq u \cup v)))$
94	93	3impd	$⊢ (φ \land u \in J \land v \in J) \to ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v)$
95	94	3expia	$⊢ (φ \land u \in J) \to (v \in J \to ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v))$
96	95	ex	$⊢ φ \to (u \in J \to (v \in J \to ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v)))$
97	96	impd	$⊢ φ \to ((u \in J \land v \in J) \to ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v))$
98	97	ralrimivv	$⊢ φ \to \forall u \in J \forall v \in J ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v)$
99		connsub	$⊢ (J \in TopOn (X) \land ⋃_{k \in A} B \subseteq X) \to (J ↾_{𝑡} ⋃_{k \in A} B \in Conn \leftrightarrow \forall u \in J \forall v \in J ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v))$
100	99	biimp3ar	$⊢ (J \in TopOn (X) \land ⋃_{k \in A} B \subseteq X \land \forall u \in J \forall v \in J ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v)) \to J ↾_{𝑡} ⋃_{k \in A} B \in Conn$
101	2 10 98 100	syl3anc	$⊢ φ \to J ↾_{𝑡} ⋃_{k \in A} B \in Conn$

Metamath Proof Explorer

Theorem iunconnlem2

Proof