kqdisj

Description: A version of imain for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	kqdisj	$⊢ (J \in TopOn (X) \land U \in J) \to F [U] \cap F [A ∖ U] = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2		imadmres	$⊢ F [dom ({F ↾}_{(A ∖ U)})] = F [A ∖ U]$
3		dmres	$⊢ dom ({F ↾}_{(A ∖ U)}) = (A ∖ U) \cap dom F$
4	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
5	4	adantr	$⊢ (J \in TopOn (X) \land U \in J) \to F Fn X$
6	5	fndmd	$⊢ (J \in TopOn (X) \land U \in J) \to dom F = X$
7	6	ineq2d	$⊢ (J \in TopOn (X) \land U \in J) \to (A ∖ U) \cap dom F = (A ∖ U) \cap X$
8	3 7	syl5eq	$⊢ (J \in TopOn (X) \land U \in J) \to dom ({F ↾}_{(A ∖ U)}) = (A ∖ U) \cap X$
9	8	imaeq2d	$⊢ (J \in TopOn (X) \land U \in J) \to F [dom ({F ↾}_{(A ∖ U)})] = F [(A ∖ U) \cap X]$
10	2 9	syl5eqr	$⊢ (J \in TopOn (X) \land U \in J) \to F [A ∖ U] = F [(A ∖ U) \cap X]$
11		indif1	$⊢ (A ∖ U) \cap X = (A \cap X) ∖ U$
12		inss2	$⊢ A \cap X \subseteq X$
13		ssdif	$⊢ A \cap X \subseteq X \to (A \cap X) ∖ U \subseteq X ∖ U$
14	12 13	ax-mp	$⊢ (A \cap X) ∖ U \subseteq X ∖ U$
15	11 14	eqsstri	$⊢ (A ∖ U) \cap X \subseteq X ∖ U$
16		imass2	$⊢ (A ∖ U) \cap X \subseteq X ∖ U \to F [(A ∖ U) \cap X] \subseteq F [X ∖ U]$
17	15 16	mp1i	$⊢ (J \in TopOn (X) \land U \in J) \to F [(A ∖ U) \cap X] \subseteq F [X ∖ U]$
18	10 17	eqsstrd	$⊢ (J \in TopOn (X) \land U \in J) \to F [A ∖ U] \subseteq F [X ∖ U]$
19		sslin	$⊢ F [A ∖ U] \subseteq F [X ∖ U] \to F [U] \cap F [A ∖ U] \subseteq F [U] \cap F [X ∖ U]$
20	18 19	syl	$⊢ (J \in TopOn (X) \land U \in J) \to F [U] \cap F [A ∖ U] \subseteq F [U] \cap F [X ∖ U]$
21		eldifn	$⊢ w \in (X ∖ U) \to \neg w \in U$
22	21	adantl	$⊢ ((J \in TopOn (X) \land U \in J) \land w \in (X ∖ U)) \to \neg w \in U$
23		simpll	$⊢ ((J \in TopOn (X) \land U \in J) \land w \in (X ∖ U)) \to J \in TopOn (X)$
24		simplr	$⊢ ((J \in TopOn (X) \land U \in J) \land w \in (X ∖ U)) \to U \in J$
25		eldifi	$⊢ w \in (X ∖ U) \to w \in X$
26	25	adantl	$⊢ ((J \in TopOn (X) \land U \in J) \land w \in (X ∖ U)) \to w \in X$
27	1	kqfvima	$⊢ (J \in TopOn (X) \land U \in J \land w \in X) \to (w \in U \leftrightarrow F (w) \in F [U])$
28	23 24 26 27	syl3anc	$⊢ ((J \in TopOn (X) \land U \in J) \land w \in (X ∖ U)) \to (w \in U \leftrightarrow F (w) \in F [U])$
29	22 28	mtbid	$⊢ ((J \in TopOn (X) \land U \in J) \land w \in (X ∖ U)) \to \neg F (w) \in F [U]$
30	29	ralrimiva	$⊢ (J \in TopOn (X) \land U \in J) \to \forall w \in (X ∖ U) \neg F (w) \in F [U]$
31		difss	$⊢ X ∖ U \subseteq X$
32		eleq1	$⊢ z = F (w) \to (z \in F [U] \leftrightarrow F (w) \in F [U])$
33	32	notbid	$⊢ z = F (w) \to (\neg z \in F [U] \leftrightarrow \neg F (w) \in F [U])$
34	33	ralima	$⊢ (F Fn X \land X ∖ U \subseteq X) \to (\forall z \in F [X ∖ U] \neg z \in F [U] \leftrightarrow \forall w \in (X ∖ U) \neg F (w) \in F [U])$
35	5 31 34	sylancl	$⊢ (J \in TopOn (X) \land U \in J) \to (\forall z \in F [X ∖ U] \neg z \in F [U] \leftrightarrow \forall w \in (X ∖ U) \neg F (w) \in F [U])$
36	30 35	mpbird	$⊢ (J \in TopOn (X) \land U \in J) \to \forall z \in F [X ∖ U] \neg z \in F [U]$
37		disjr	$⊢ F [U] \cap F [X ∖ U] = \emptyset \leftrightarrow \forall z \in F [X ∖ U] \neg z \in F [U]$
38	36 37	sylibr	$⊢ (J \in TopOn (X) \land U \in J) \to F [U] \cap F [X ∖ U] = \emptyset$
39		sseq0	$⊢ (F [U] \cap F [A ∖ U] \subseteq F [U] \cap F [X ∖ U] \land F [U] \cap F [X ∖ U] = \emptyset) \to F [U] \cap F [A ∖ U] = \emptyset$
40	20 38 39	syl2anc	$⊢ (J \in TopOn (X) \land U \in J) \to F [U] \cap F [A ∖ U] = \emptyset$

Metamath Proof Explorer

Theorem kqdisj

Proof