iunconnlem

	Ref	Expression
Hypotheses	iunconn.2	$⊢ φ \to J \in TopOn (X)$
	iunconn.3	$⊢ (φ \land k \in A) \to B \subseteq X$
	iunconn.4	$⊢ (φ \land k \in A) \to P \in B$
	iunconn.5	$⊢ (φ \land k \in A) \to J ↾_{𝑡} B \in Conn$
	iunconn.6	$⊢ φ \to U \in J$
	iunconn.7	$⊢ φ \to V \in J$
	iunconn.8	$⊢ φ \to V \cap ⋃_{k \in A} B \neq \emptyset$
	iunconn.9	$⊢ φ \to U \cap V \subseteq X ∖ ⋃_{k \in A} B$
	iunconn.10	$⊢ φ \to ⋃_{k \in A} B \subseteq U \cup V$
	iunconn.11	$⊢ Ⅎ k φ$
Assertion	iunconnlem	$⊢ φ \to \neg P \in U$

Proof

Step	Hyp	Ref	Expression
1		iunconn.2	$⊢ φ \to J \in TopOn (X)$
2		iunconn.3	$⊢ (φ \land k \in A) \to B \subseteq X$
3		iunconn.4	$⊢ (φ \land k \in A) \to P \in B$
4		iunconn.5	$⊢ (φ \land k \in A) \to J ↾_{𝑡} B \in Conn$
5		iunconn.6	$⊢ φ \to U \in J$
6		iunconn.7	$⊢ φ \to V \in J$
7		iunconn.8	$⊢ φ \to V \cap ⋃_{k \in A} B \neq \emptyset$
8		iunconn.9	$⊢ φ \to U \cap V \subseteq X ∖ ⋃_{k \in A} B$
9		iunconn.10	$⊢ φ \to ⋃_{k \in A} B \subseteq U \cup V$
10		iunconn.11	$⊢ Ⅎ k φ$
11		n0	$⊢ V \cap ⋃_{k \in A} B \neq \emptyset \leftrightarrow \exists x x \in (V \cap ⋃_{k \in A} B)$
12	7 11	sylib	$⊢ φ \to \exists x x \in (V \cap ⋃_{k \in A} B)$
13		elin	$⊢ x \in (V \cap ⋃_{k \in A} B) \leftrightarrow (x \in V \land x \in ⋃_{k \in A} B)$
14		eliun	$⊢ x \in ⋃_{k \in A} B \leftrightarrow \exists k \in A x \in B$
15		nfv	$⊢ Ⅎ k x \in V$
16	10 15	nfan	$⊢ Ⅎ k (φ \land x \in V)$
17		nfv	$⊢ Ⅎ k \neg P \in U$
18	4	adantr	$⊢ ((φ \land k \in A) \land (x \in V \land x \in B)) \to J ↾_{𝑡} B \in Conn$
19	1	ad2antrr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to J \in TopOn (X)$
20	2	adantr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to B \subseteq X$
21	5	ad2antrr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to U \in J$
22	6	ad2antrr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to V \in J$
23		simprr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to P \in U$
24	3	adantr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to P \in B$
25		inelcm	$⊢ (P \in U \land P \in B) \to U \cap B \neq \emptyset$
26	23 24 25	syl2anc	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to U \cap B \neq \emptyset$
27		inelcm	$⊢ (x \in V \land x \in B) \to V \cap B \neq \emptyset$
28	27	ad2antrl	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to V \cap B \neq \emptyset$
29	8	ad2antrr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to U \cap V \subseteq X ∖ ⋃_{k \in A} B$
30		ssiun2	$⊢ k \in A \to B \subseteq ⋃_{k \in A} B$
31	30	ad2antlr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to B \subseteq ⋃_{k \in A} B$
32	31	sscond	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to X ∖ ⋃_{k \in A} B \subseteq X ∖ B$
33	29 32	sstrd	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to U \cap V \subseteq X ∖ B$
34		inss1	$⊢ U \cap V \subseteq U$
35		toponss	$⊢ (J \in TopOn (X) \land U \in J) \to U \subseteq X$
36	19 21 35	syl2anc	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to U \subseteq X$
37	34 36	sstrid	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to U \cap V \subseteq X$
38		reldisj	$⊢ U \cap V \subseteq X \to ((U \cap V) \cap B = \emptyset \leftrightarrow U \cap V \subseteq X ∖ B)$
39	37 38	syl	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to ((U \cap V) \cap B = \emptyset \leftrightarrow U \cap V \subseteq X ∖ B)$
40	33 39	mpbird	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to (U \cap V) \cap B = \emptyset$
41	9	ad2antrr	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to ⋃_{k \in A} B \subseteq U \cup V$
42	31 41	sstrd	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to B \subseteq U \cup V$
43	19 20 21 22 26 28 40 42	nconnsubb	$⊢ ((φ \land k \in A) \land ((x \in V \land x \in B) \land P \in U)) \to \neg J ↾_{𝑡} B \in Conn$
44	43	expr	$⊢ ((φ \land k \in A) \land (x \in V \land x \in B)) \to (P \in U \to \neg J ↾_{𝑡} B \in Conn)$
45	18 44	mt2d	$⊢ ((φ \land k \in A) \land (x \in V \land x \in B)) \to \neg P \in U$
46	45	an4s	$⊢ ((φ \land x \in V) \land (k \in A \land x \in B)) \to \neg P \in U$
47	46	exp32	$⊢ (φ \land x \in V) \to (k \in A \to (x \in B \to \neg P \in U))$
48	16 17 47	rexlimd	$⊢ (φ \land x \in V) \to (\exists k \in A x \in B \to \neg P \in U)$
49	14 48	syl5bi	$⊢ (φ \land x \in V) \to (x \in ⋃_{k \in A} B \to \neg P \in U)$
50	49	expimpd	$⊢ φ \to ((x \in V \land x \in ⋃_{k \in A} B) \to \neg P \in U)$
51	13 50	syl5bi	$⊢ φ \to (x \in (V \cap ⋃_{k \in A} B) \to \neg P \in U)$
52	51	exlimdv	$⊢ φ \to (\exists x x \in (V \cap ⋃_{k \in A} B) \to \neg P \in U)$
53	12 52	mpd	$⊢ φ \to \neg P \in U$

Metamath Proof Explorer

Theorem iunconnlem

Proof