mreexexlem2d

Description: Used in mreexexlem4d to prove the induction step in mreexexd . See the proof of Proposition 4.2.1 in FaureFrolicher p. 86 to 87. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mreexexlem2d.1	$⊢ φ \to A \in Moore (X)$
	mreexexlem2d.2	$⊢ N = mrCls (A)$
	mreexexlem2d.3	$⊢ I = mrInd (A)$
	mreexexlem2d.4	$⊢ φ \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
	mreexexlem2d.5	$⊢ φ \to F \subseteq X ∖ H$
	mreexexlem2d.6	$⊢ φ \to G \subseteq X ∖ H$
	mreexexlem2d.7	$⊢ φ \to F \subseteq N (G \cup H)$
	mreexexlem2d.8	$⊢ φ \to F \cup H \in I$
	mreexexlem2d.9	$⊢ φ \to Y \in F$
Assertion	mreexexlem2d	$⊢ φ \to \exists g \in G (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I)$

Proof

Step	Hyp	Ref	Expression
1		mreexexlem2d.1	$⊢ φ \to A \in Moore (X)$
2		mreexexlem2d.2	$⊢ N = mrCls (A)$
3		mreexexlem2d.3	$⊢ I = mrInd (A)$
4		mreexexlem2d.4	$⊢ φ \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
5		mreexexlem2d.5	$⊢ φ \to F \subseteq X ∖ H$
6		mreexexlem2d.6	$⊢ φ \to G \subseteq X ∖ H$
7		mreexexlem2d.7	$⊢ φ \to F \subseteq N (G \cup H)$
8		mreexexlem2d.8	$⊢ φ \to F \cup H \in I$
9		mreexexlem2d.9	$⊢ φ \to Y \in F$
10	7	adantr	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to F \subseteq N (G \cup H)$
11	1	adantr	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to A \in Moore (X)$
12		simpr	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to G \subseteq N ((F \cup H) ∖ \{Y\})$
13		ssun2	$⊢ H \subseteq (F ∖ \{Y\}) \cup H$
14		difundir	$⊢ (F \cup H) ∖ \{Y\} = (F ∖ \{Y\}) \cup (H ∖ \{Y\})$
15		incom	$⊢ F \cap H = H \cap F$
16		ssdifin0	$⊢ F \subseteq X ∖ H \to F \cap H = \emptyset$
17	5 16	syl	$⊢ φ \to F \cap H = \emptyset$
18	15 17	eqtr3id	$⊢ φ \to H \cap F = \emptyset$
19		minel	$⊢ (Y \in F \land H \cap F = \emptyset) \to \neg Y \in H$
20	9 18 19	syl2anc	$⊢ φ \to \neg Y \in H$
21		difsnb	$⊢ \neg Y \in H \leftrightarrow H ∖ \{Y\} = H$
22	20 21	sylib	$⊢ φ \to H ∖ \{Y\} = H$
23	22	uneq2d	$⊢ φ \to (F ∖ \{Y\}) \cup (H ∖ \{Y\}) = (F ∖ \{Y\}) \cup H$
24	14 23	eqtrid	$⊢ φ \to (F \cup H) ∖ \{Y\} = (F ∖ \{Y\}) \cup H$
25	13 24	sseqtrrid	$⊢ φ \to H \subseteq (F \cup H) ∖ \{Y\}$
26	3 1 8	mrissd	$⊢ φ \to F \cup H \subseteq X$
27	26	ssdifssd	$⊢ φ \to (F \cup H) ∖ \{Y\} \subseteq X$
28	1 2 27	mrcssidd	$⊢ φ \to (F \cup H) ∖ \{Y\} \subseteq N ((F \cup H) ∖ \{Y\})$
29	25 28	sstrd	$⊢ φ \to H \subseteq N ((F \cup H) ∖ \{Y\})$
30	29	adantr	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to H \subseteq N ((F \cup H) ∖ \{Y\})$
31	12 30	unssd	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to G \cup H \subseteq N ((F \cup H) ∖ \{Y\})$
32	11 2	mrcssvd	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to N ((F \cup H) ∖ \{Y\}) \subseteq X$
33	11 2 31 32	mrcssd	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to N (G \cup H) \subseteq N (N ((F \cup H) ∖ \{Y\}))$
34	27	adantr	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to (F \cup H) ∖ \{Y\} \subseteq X$
35	11 2 34	mrcidmd	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to N (N ((F \cup H) ∖ \{Y\})) = N ((F \cup H) ∖ \{Y\})$
36	33 35	sseqtrd	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to N (G \cup H) \subseteq N ((F \cup H) ∖ \{Y\})$
37	10 36	sstrd	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to F \subseteq N ((F \cup H) ∖ \{Y\})$
38	9	adantr	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to Y \in F$
39	37 38	sseldd	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to Y \in N ((F \cup H) ∖ \{Y\})$
40	8	adantr	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to F \cup H \in I$
41		ssun1	$⊢ F \subseteq F \cup H$
42	41 38	sselid	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to Y \in (F \cup H)$
43	2 3 11 40 42	ismri2dad	$⊢ (φ \land G \subseteq N ((F \cup H) ∖ \{Y\})) \to \neg Y \in N ((F \cup H) ∖ \{Y\})$
44	39 43	pm2.65da	$⊢ φ \to \neg G \subseteq N ((F \cup H) ∖ \{Y\})$
45		nss	$⊢ \neg G \subseteq N ((F \cup H) ∖ \{Y\}) \leftrightarrow \exists g (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))$
46	44 45	sylib	$⊢ φ \to \exists g (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))$
47		simprl	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to g \in G$
48		ssun1	$⊢ F ∖ \{Y\} \subseteq (F ∖ \{Y\}) \cup H$
49	48 24	sseqtrrid	$⊢ φ \to F ∖ \{Y\} \subseteq (F \cup H) ∖ \{Y\}$
50	49 28	sstrd	$⊢ φ \to F ∖ \{Y\} \subseteq N ((F \cup H) ∖ \{Y\})$
51	50	adantr	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to F ∖ \{Y\} \subseteq N ((F \cup H) ∖ \{Y\})$
52		simprr	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to \neg g \in N ((F \cup H) ∖ \{Y\})$
53	51 52	ssneldd	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to \neg g \in (F ∖ \{Y\})$
54		unass	$⊢ ((F ∖ \{Y\}) \cup H) \cup \{g\} = (F ∖ \{Y\}) \cup (H \cup \{g\})$
55	1	adantr	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to A \in Moore (X)$
56	4	adantr	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
57	8	adantr	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to F \cup H \in I$
58		difss	$⊢ F ∖ \{Y\} \subseteq F$
59		unss1	$⊢ F ∖ \{Y\} \subseteq F \to (F ∖ \{Y\}) \cup H \subseteq F \cup H$
60	58 59	mp1i	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to (F ∖ \{Y\}) \cup H \subseteq F \cup H$
61	55 2 3 57 60	mrissmrid	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to (F ∖ \{Y\}) \cup H \in I$
62	6	adantr	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to G \subseteq X ∖ H$
63	62	difss2d	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to G \subseteq X$
64	63 47	sseldd	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to g \in X$
65	24	adantr	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to (F \cup H) ∖ \{Y\} = (F ∖ \{Y\}) \cup H$
66	65	fveq2d	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to N ((F \cup H) ∖ \{Y\}) = N ((F ∖ \{Y\}) \cup H)$
67	52 66	neleqtrd	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to \neg g \in N ((F ∖ \{Y\}) \cup H)$
68	55 2 3 56 61 64 67	mreexmrid	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to ((F ∖ \{Y\}) \cup H) \cup \{g\} \in I$
69	54 68	eqeltrrid	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I$
70	47 53 69	jca32	$⊢ (φ \land (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\}))) \to (g \in G \land (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I))$
71	70	ex	$⊢ φ \to ((g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\})) \to (g \in G \land (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I)))$
72	71	eximdv	$⊢ φ \to (\exists g (g \in G \land \neg g \in N ((F \cup H) ∖ \{Y\})) \to \exists g (g \in G \land (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I)))$
73	46 72	mpd	$⊢ φ \to \exists g (g \in G \land (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I))$
74		df-rex	$⊢ \exists g \in G (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I) \leftrightarrow \exists g (g \in G \land (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I))$
75	73 74	sylibr	$⊢ φ \to \exists g \in G (\neg g \in (F ∖ \{Y\}) \land (F ∖ \{Y\}) \cup (H \cup \{g\}) \in I)$

Metamath Proof Explorer

Theorem mreexexlem2d

Proof