mreexexlem3d

Description: Base case of the induction in mreexexd . (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$
	mreexexlem3d.9	$⊢ φ \to (F = \emptyset \lor G = \emptyset)$
Assertion	mreexexlem3d	$⊢ φ \to \exists i \in 𝒫 G (F \approx i \land i \cup H \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		mreexexlem3d.9	$⊢ φ \to (F = \emptyset \lor G = \emptyset)$
10		simpr	$⊢ (φ \land F = \emptyset) \to F = \emptyset$
11	1	adantr	$⊢ (φ \land G = \emptyset) \to A \in Moore (X)$
12	7	adantr	$⊢ (φ \land G = \emptyset) \to F \subseteq N (G \cup H)$
13		simpr	$⊢ (φ \land G = \emptyset) \to G = \emptyset$
14	13	uneq1d	$⊢ (φ \land G = \emptyset) \to G \cup H = \emptyset \cup H$
15		uncom	$⊢ H \cup \emptyset = \emptyset \cup H$
16		un0	$⊢ H \cup \emptyset = H$
17	15 16	eqtr3i	$⊢ \emptyset \cup H = H$
18	14 17	eqtrdi	$⊢ (φ \land G = \emptyset) \to G \cup H = H$
19	18	fveq2d	$⊢ (φ \land G = \emptyset) \to N (G \cup H) = N (H)$
20	12 19	sseqtrd	$⊢ (φ \land G = \emptyset) \to F \subseteq N (H)$
21	8	adantr	$⊢ (φ \land G = \emptyset) \to F \cup H \in I$
22	3 11 21	mrissd	$⊢ (φ \land G = \emptyset) \to F \cup H \subseteq X$
23	22	unssbd	$⊢ (φ \land G = \emptyset) \to H \subseteq X$
24	11 2 23	mrcssidd	$⊢ (φ \land G = \emptyset) \to H \subseteq N (H)$
25	20 24	unssd	$⊢ (φ \land G = \emptyset) \to F \cup H \subseteq N (H)$
26		ssun2	$⊢ H \subseteq F \cup H$
27	26	a1i	$⊢ (φ \land G = \emptyset) \to H \subseteq F \cup H$
28	11 2 3 25 27 21	mrissmrcd	$⊢ (φ \land G = \emptyset) \to F \cup H = H$
29		ssequn1	$⊢ F \subseteq H \leftrightarrow F \cup H = H$
30	28 29	sylibr	$⊢ (φ \land G = \emptyset) \to F \subseteq H$
31	5	adantr	$⊢ (φ \land G = \emptyset) \to F \subseteq X ∖ H$
32	30 31	ssind	$⊢ (φ \land G = \emptyset) \to F \subseteq H \cap (X ∖ H)$
33		disjdif	$⊢ H \cap (X ∖ H) = \emptyset$
34	32 33	sseqtrdi	$⊢ (φ \land G = \emptyset) \to F \subseteq \emptyset$
35		ss0b	$⊢ F \subseteq \emptyset \leftrightarrow F = \emptyset$
36	34 35	sylib	$⊢ (φ \land G = \emptyset) \to F = \emptyset$
37	10 36 9	mpjaodan	$⊢ φ \to F = \emptyset$
38		0elpw	$⊢ \emptyset \in 𝒫 G$
39	37 38	eqeltrdi	$⊢ φ \to F \in 𝒫 G$
40	1	elfvexd	$⊢ φ \to X \in V$
41	5	difss2d	$⊢ φ \to F \subseteq X$
42	40 41	ssexd	$⊢ φ \to F \in V$
43		enrefg	$⊢ F \in V \to F \approx F$
44	42 43	syl	$⊢ φ \to F \approx F$
45		breq2	$⊢ i = F \to (F \approx i \leftrightarrow F \approx F)$
46		uneq1	$⊢ i = F \to i \cup H = F \cup H$
47	46	eleq1d	$⊢ i = F \to (i \cup H \in I \leftrightarrow F \cup H \in I)$
48	45 47	anbi12d	$⊢ i = F \to ((F \approx i \land i \cup H \in I) \leftrightarrow (F \approx F \land F \cup H \in I))$
49	48	rspcev	$⊢ (F \in 𝒫 G \land (F \approx F \land F \cup H \in I)) \to \exists i \in 𝒫 G (F \approx i \land i \cup H \in I)$
50	39 44 8 49	syl12anc	$⊢ φ \to \exists i \in 𝒫 G (F \approx i \land i \cup H \in I)$

Metamath Proof Explorer

Theorem mreexexlem3d

Proof