regr1lem

	Ref	Expression
Hypotheses	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	regr1lem.2	$⊢ φ \to J \in TopOn (X)$
	regr1lem.3	$⊢ φ \to J \in Reg$
	regr1lem.4	$⊢ φ \to A \in X$
	regr1lem.5	$⊢ φ \to B \in X$
	regr1lem.6	$⊢ φ \to U \in J$
	regr1lem.7	$⊢ φ \to \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (A) \in m \land F (B) \in n \land m \cap n = \emptyset)$
Assertion	regr1lem	$⊢ φ \to (A \in U \to B \in U)$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2		regr1lem.2	$⊢ φ \to J \in TopOn (X)$
3		regr1lem.3	$⊢ φ \to J \in Reg$
4		regr1lem.4	$⊢ φ \to A \in X$
5		regr1lem.5	$⊢ φ \to B \in X$
6		regr1lem.6	$⊢ φ \to U \in J$
7		regr1lem.7	$⊢ φ \to \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (A) \in m \land F (B) \in n \land m \cap n = \emptyset)$
8	3	adantr	$⊢ (φ \land A \in U) \to J \in Reg$
9	6	adantr	$⊢ (φ \land A \in U) \to U \in J$
10		simpr	$⊢ (φ \land A \in U) \to A \in U$
11		regsep	$⊢ (J \in Reg \land U \in J \land A \in U) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq U)$
12	8 9 10 11	syl3anc	$⊢ (φ \land A \in U) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq U)$
13	7	ad2antrr	$⊢ ((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \to \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (A) \in m \land F (B) \in n \land m \cap n = \emptyset)$
14	2	ad3antrrr	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to J \in TopOn (X)$
15		simplrl	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to z \in J$
16	1	kqopn	$⊢ (J \in TopOn (X) \land z \in J) \to F [z] \in KQ (J)$
17	14 15 16	syl2anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to F [z] \in KQ (J)$
18		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
19	14 18	syl	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to X = ⋃ J$
20	19	difeq1d	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to X ∖ cls (J) (z) = ⋃ J ∖ cls (J) (z)$
21		topontop	$⊢ J \in TopOn (X) \to J \in Top$
22	14 21	syl	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to J \in Top$
23		elssuni	$⊢ z \in J \to z \subseteq ⋃ J$
24	15 23	syl	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to z \subseteq ⋃ J$
25		eqid	$⊢ ⋃ J = ⋃ J$
26	25	clscld	$⊢ (J \in Top \land z \subseteq ⋃ J) \to cls (J) (z) \in Clsd (J)$
27	22 24 26	syl2anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to cls (J) (z) \in Clsd (J)$
28	25	cldopn	$⊢ cls (J) (z) \in Clsd (J) \to ⋃ J ∖ cls (J) (z) \in J$
29	27 28	syl	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to ⋃ J ∖ cls (J) (z) \in J$
30	20 29	eqeltrd	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to X ∖ cls (J) (z) \in J$
31	1	kqopn	$⊢ (J \in TopOn (X) \land X ∖ cls (J) (z) \in J) \to F [X ∖ cls (J) (z)] \in KQ (J)$
32	14 30 31	syl2anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to F [X ∖ cls (J) (z)] \in KQ (J)$
33		simprrl	$⊢ ((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \to A \in z$
34	33	adantr	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to A \in z$
35	4	ad3antrrr	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to A \in X$
36	1	kqfvima	$⊢ (J \in TopOn (X) \land z \in J \land A \in X) \to (A \in z \leftrightarrow F (A) \in F [z])$
37	14 15 35 36	syl3anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to (A \in z \leftrightarrow F (A) \in F [z])$
38	34 37	mpbid	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to F (A) \in F [z]$
39	5	ad3antrrr	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to B \in X$
40		simprrr	$⊢ ((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \to cls (J) (z) \subseteq U$
41	40	sseld	$⊢ ((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \to (B \in cls (J) (z) \to B \in U)$
42	41	con3dimp	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to \neg B \in cls (J) (z)$
43	39 42	eldifd	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to B \in (X ∖ cls (J) (z))$
44	1	kqfvima	$⊢ (J \in TopOn (X) \land X ∖ cls (J) (z) \in J \land B \in X) \to (B \in (X ∖ cls (J) (z)) \leftrightarrow F (B) \in F [X ∖ cls (J) (z)])$
45	14 30 39 44	syl3anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to (B \in (X ∖ cls (J) (z)) \leftrightarrow F (B) \in F [X ∖ cls (J) (z)])$
46	43 45	mpbid	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to F (B) \in F [X ∖ cls (J) (z)]$
47	25	sscls	$⊢ (J \in Top \land z \subseteq ⋃ J) \to z \subseteq cls (J) (z)$
48	22 24 47	syl2anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to z \subseteq cls (J) (z)$
49	48	sscond	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to X ∖ cls (J) (z) \subseteq X ∖ z$
50		imass2	$⊢ X ∖ cls (J) (z) \subseteq X ∖ z \to F [X ∖ cls (J) (z)] \subseteq F [X ∖ z]$
51		sslin	$⊢ F [X ∖ cls (J) (z)] \subseteq F [X ∖ z] \to F [z] \cap F [X ∖ cls (J) (z)] \subseteq F [z] \cap F [X ∖ z]$
52	49 50 51	3syl	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to F [z] \cap F [X ∖ cls (J) (z)] \subseteq F [z] \cap F [X ∖ z]$
53	1	kqdisj	$⊢ (J \in TopOn (X) \land z \in J) \to F [z] \cap F [X ∖ z] = \emptyset$
54	14 15 53	syl2anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to F [z] \cap F [X ∖ z] = \emptyset$
55		sseq0	$⊢ (F [z] \cap F [X ∖ cls (J) (z)] \subseteq F [z] \cap F [X ∖ z] \land F [z] \cap F [X ∖ z] = \emptyset) \to F [z] \cap F [X ∖ cls (J) (z)] = \emptyset$
56	52 54 55	syl2anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to F [z] \cap F [X ∖ cls (J) (z)] = \emptyset$
57		eleq2	$⊢ m = F [z] \to (F (A) \in m \leftrightarrow F (A) \in F [z])$
58		ineq1	$⊢ m = F [z] \to m \cap n = F [z] \cap n$
59	58	eqeq1d	$⊢ m = F [z] \to (m \cap n = \emptyset \leftrightarrow F [z] \cap n = \emptyset)$
60	57 59	3anbi13d	$⊢ m = F [z] \to ((F (A) \in m \land F (B) \in n \land m \cap n = \emptyset) \leftrightarrow (F (A) \in F [z] \land F (B) \in n \land F [z] \cap n = \emptyset))$
61		eleq2	$⊢ n = F [X ∖ cls (J) (z)] \to (F (B) \in n \leftrightarrow F (B) \in F [X ∖ cls (J) (z)])$
62		ineq2	$⊢ n = F [X ∖ cls (J) (z)] \to F [z] \cap n = F [z] \cap F [X ∖ cls (J) (z)]$
63	62	eqeq1d	$⊢ n = F [X ∖ cls (J) (z)] \to (F [z] \cap n = \emptyset \leftrightarrow F [z] \cap F [X ∖ cls (J) (z)] = \emptyset)$
64	61 63	3anbi23d	$⊢ n = F [X ∖ cls (J) (z)] \to ((F (A) \in F [z] \land F (B) \in n \land F [z] \cap n = \emptyset) \leftrightarrow (F (A) \in F [z] \land F (B) \in F [X ∖ cls (J) (z)] \land F [z] \cap F [X ∖ cls (J) (z)] = \emptyset))$
65	60 64	rspc2ev	$⊢ (F [z] \in KQ (J) \land F [X ∖ cls (J) (z)] \in KQ (J) \land (F (A) \in F [z] \land F (B) \in F [X ∖ cls (J) (z)] \land F [z] \cap F [X ∖ cls (J) (z)] = \emptyset)) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (A) \in m \land F (B) \in n \land m \cap n = \emptyset)$
66	17 32 38 46 56 65	syl113anc	$⊢ (((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \land \neg B \in U) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (A) \in m \land F (B) \in n \land m \cap n = \emptyset)$
67	66	ex	$⊢ ((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \to (\neg B \in U \to \exists m \in KQ (J) \exists n \in KQ (J) (F (A) \in m \land F (B) \in n \land m \cap n = \emptyset))$
68	13 67	mt3d	$⊢ ((φ \land A \in U) \land (z \in J \land (A \in z \land cls (J) (z) \subseteq U))) \to B \in U$
69	12 68	rexlimddv	$⊢ (φ \land A \in U) \to B \in U$
70	69	ex	$⊢ φ \to (A \in U \to B \in U)$

Metamath Proof Explorer

Theorem regr1lem

Proof