mreexexlem4d

Description: Induction step 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$
	mreexexlem4d.9	$⊢ φ \to L \in ω$
	mreexexlem4d.A	$⊢ φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx L \lor g \approx L) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I))$
	mreexexlem4d.B	$⊢ φ \to (F \approx suc L \lor G \approx suc L)$
Assertion	mreexexlem4d	$⊢ φ \to \exists j \in 𝒫 G (F \approx j \land j \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		mreexexlem4d.9	$⊢ φ \to L \in ω$
10		mreexexlem4d.A	$⊢ φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx L \lor g \approx L) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I))$
11		mreexexlem4d.B	$⊢ φ \to (F \approx suc L \lor G \approx suc L)$
12	1	adantr	$⊢ (φ \land F = \emptyset) \to A \in Moore (X)$
13	4	adantr	$⊢ (φ \land F = \emptyset) \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
14	5	adantr	$⊢ (φ \land F = \emptyset) \to F \subseteq X ∖ H$
15	6	adantr	$⊢ (φ \land F = \emptyset) \to G \subseteq X ∖ H$
16	7	adantr	$⊢ (φ \land F = \emptyset) \to F \subseteq N (G \cup H)$
17	8	adantr	$⊢ (φ \land F = \emptyset) \to F \cup H \in I$
18		animorrl	$⊢ (φ \land F = \emptyset) \to (F = \emptyset \lor G = \emptyset)$
19	12 2 3 13 14 15 16 17 18	mreexexlem3d	$⊢ (φ \land F = \emptyset) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
20		n0	$⊢ F \neq \emptyset \leftrightarrow \exists r r \in F$
21	20	biimpi	$⊢ F \neq \emptyset \to \exists r r \in F$
22	21	adantl	$⊢ (φ \land F \neq \emptyset) \to \exists r r \in F$
23	1	adantr	$⊢ (φ \land r \in F) \to A \in Moore (X)$
24	4	adantr	$⊢ (φ \land r \in F) \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
25	5	adantr	$⊢ (φ \land r \in F) \to F \subseteq X ∖ H$
26	6	adantr	$⊢ (φ \land r \in F) \to G \subseteq X ∖ H$
27	7	adantr	$⊢ (φ \land r \in F) \to F \subseteq N (G \cup H)$
28	8	adantr	$⊢ (φ \land r \in F) \to F \cup H \in I$
29		simpr	$⊢ (φ \land r \in F) \to r \in F$
30	23 2 3 24 25 26 27 28 29	mreexexlem2d	$⊢ (φ \land r \in F) \to \exists q \in G (\neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)$
31		3anass	$⊢ (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I) \leftrightarrow (q \in G \land (\neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I))$
32	1	ad2antrr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to A \in Moore (X)$
33	32	elfvexd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to X \in V$
34		simpr2	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to \neg q \in (F ∖ \{r\})$
35		difsnb	$⊢ \neg q \in (F ∖ \{r\}) \leftrightarrow (F ∖ \{r\}) ∖ \{q\} = F ∖ \{r\}$
36	34 35	sylib	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to (F ∖ \{r\}) ∖ \{q\} = F ∖ \{r\}$
37	5	ad2antrr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to F \subseteq X ∖ H$
38	37	ssdifssd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to F ∖ \{r\} \subseteq X ∖ H$
39	38	ssdifd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to (F ∖ \{r\}) ∖ \{q\} \subseteq (X ∖ H) ∖ \{q\}$
40	36 39	eqsstrrd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to F ∖ \{r\} \subseteq (X ∖ H) ∖ \{q\}$
41		difun1	$⊢ X ∖ (H \cup \{q\}) = (X ∖ H) ∖ \{q\}$
42	40 41	sseqtrrdi	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to F ∖ \{r\} \subseteq X ∖ (H \cup \{q\})$
43	6	ad2antrr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to G \subseteq X ∖ H$
44	43	ssdifd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to G ∖ \{q\} \subseteq (X ∖ H) ∖ \{q\}$
45	44 41	sseqtrrdi	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to G ∖ \{q\} \subseteq X ∖ (H \cup \{q\})$
46	7	ad2antrr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to F \subseteq N (G \cup H)$
47		simpr1	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to q \in G$
48		uncom	$⊢ H \cup \{q\} = \{q\} \cup H$
49	48	uneq2i	$⊢ (G ∖ \{q\}) \cup (H \cup \{q\}) = (G ∖ \{q\}) \cup (\{q\} \cup H)$
50		unass	$⊢ ((G ∖ \{q\}) \cup \{q\}) \cup H = (G ∖ \{q\}) \cup (\{q\} \cup H)$
51		difsnid	$⊢ q \in G \to (G ∖ \{q\}) \cup \{q\} = G$
52	51	uneq1d	$⊢ q \in G \to ((G ∖ \{q\}) \cup \{q\}) \cup H = G \cup H$
53	50 52	eqtr3id	$⊢ q \in G \to (G ∖ \{q\}) \cup (\{q\} \cup H) = G \cup H$
54	49 53	eqtrid	$⊢ q \in G \to (G ∖ \{q\}) \cup (H \cup \{q\}) = G \cup H$
55	47 54	syl	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to (G ∖ \{q\}) \cup (H \cup \{q\}) = G \cup H$
56	55	fveq2d	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to N ((G ∖ \{q\}) \cup (H \cup \{q\})) = N (G \cup H)$
57	46 56	sseqtrrd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to F \subseteq N ((G ∖ \{q\}) \cup (H \cup \{q\}))$
58	57	ssdifssd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to F ∖ \{r\} \subseteq N ((G ∖ \{q\}) \cup (H \cup \{q\}))$
59		simpr3	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to (F ∖ \{r\}) \cup (H \cup \{q\}) \in I$
60	11	ad2antrr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to (F \approx suc L \lor G \approx suc L)$
61	9	ad2antrr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to L \in ω$
62		simplr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to r \in F$
63		3anan12	$⊢ (L \in ω \land F \approx suc L \land r \in F) \leftrightarrow (F \approx suc L \land (L \in ω \land r \in F))$
64		dif1en	$⊢ (L \in ω \land F \approx suc L \land r \in F) \to (F ∖ \{r\}) \approx L$
65	63 64	sylbir	$⊢ (F \approx suc L \land (L \in ω \land r \in F)) \to (F ∖ \{r\}) \approx L$
66	65	expcom	$⊢ (L \in ω \land r \in F) \to (F \approx suc L \to (F ∖ \{r\}) \approx L)$
67	61 62 66	syl2anc	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to (F \approx suc L \to (F ∖ \{r\}) \approx L)$
68		3anan12	$⊢ (L \in ω \land G \approx suc L \land q \in G) \leftrightarrow (G \approx suc L \land (L \in ω \land q \in G))$
69		dif1en	$⊢ (L \in ω \land G \approx suc L \land q \in G) \to (G ∖ \{q\}) \approx L$
70	68 69	sylbir	$⊢ (G \approx suc L \land (L \in ω \land q \in G)) \to (G ∖ \{q\}) \approx L$
71	70	expcom	$⊢ (L \in ω \land q \in G) \to (G \approx suc L \to (G ∖ \{q\}) \approx L)$
72	61 47 71	syl2anc	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to (G \approx suc L \to (G ∖ \{q\}) \approx L)$
73	67 72	orim12d	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to ((F \approx suc L \lor G \approx suc L) \to ((F ∖ \{r\}) \approx L \lor (G ∖ \{q\}) \approx L))$
74	60 73	mpd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to ((F ∖ \{r\}) \approx L \lor (G ∖ \{q\}) \approx L)$
75	10	ad2antrr	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx L \lor g \approx L) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I))$
76	33 42 45 58 59 74 75	mreexexlemd	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to \exists i \in 𝒫 (G ∖ \{q\}) ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I)$
77	33	adantr	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to X \in V$
78	6	ad3antrrr	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to G \subseteq X ∖ H$
79	78	difss2d	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to G \subseteq X$
80	77 79	ssexd	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to G \in V$
81		simprl	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to i \in 𝒫 (G ∖ \{q\})$
82	81	elpwid	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to i \subseteq G ∖ \{q\}$
83	82	difss2d	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to i \subseteq G$
84		simplr1	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to q \in G$
85	84	snssd	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to \{q\} \subseteq G$
86	83 85	unssd	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to i \cup \{q\} \subseteq G$
87	80 86	sselpwd	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to i \cup \{q\} \in 𝒫 G$
88		difsnid	$⊢ r \in F \to (F ∖ \{r\}) \cup \{r\} = F$
89	88	ad3antlr	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to (F ∖ \{r\}) \cup \{r\} = F$
90		simprrl	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to (F ∖ \{r\}) \approx i$
91		en2sn	$⊢ (r \in V \land q \in V) \to \{r\} \approx \{q\}$
92	91	el2v	$⊢ \{r\} \approx \{q\}$
93	92	a1i	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to \{r\} \approx \{q\}$
94		disjdifr	$⊢ (F ∖ \{r\}) \cap \{r\} = \emptyset$
95	94	a1i	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to (F ∖ \{r\}) \cap \{r\} = \emptyset$
96		ssdifin0	$⊢ i \subseteq G ∖ \{q\} \to i \cap \{q\} = \emptyset$
97	82 96	syl	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to i \cap \{q\} = \emptyset$
98		unen	$⊢ (((F ∖ \{r\}) \approx i \land \{r\} \approx \{q\}) \land ((F ∖ \{r\}) \cap \{r\} = \emptyset \land i \cap \{q\} = \emptyset)) \to ((F ∖ \{r\}) \cup \{r\}) \approx (i \cup \{q\})$
99	90 93 95 97 98	syl22anc	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to ((F ∖ \{r\}) \cup \{r\}) \approx (i \cup \{q\})$
100	89 99	eqbrtrrd	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to F \approx (i \cup \{q\})$
101		unass	$⊢ (i \cup \{q\}) \cup H = i \cup (\{q\} \cup H)$
102		uncom	$⊢ \{q\} \cup H = H \cup \{q\}$
103	102	uneq2i	$⊢ i \cup (\{q\} \cup H) = i \cup (H \cup \{q\})$
104	101 103	eqtr2i	$⊢ i \cup (H \cup \{q\}) = (i \cup \{q\}) \cup H$
105		simprrr	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to i \cup (H \cup \{q\}) \in I$
106	104 105	eqeltrrid	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to (i \cup \{q\}) \cup H \in I$
107		breq2	$⊢ j = i \cup \{q\} \to (F \approx j \leftrightarrow F \approx (i \cup \{q\}))$
108		uneq1	$⊢ j = i \cup \{q\} \to j \cup H = (i \cup \{q\}) \cup H$
109	108	eleq1d	$⊢ j = i \cup \{q\} \to (j \cup H \in I \leftrightarrow (i \cup \{q\}) \cup H \in I)$
110	107 109	anbi12d	$⊢ j = i \cup \{q\} \to ((F \approx j \land j \cup H \in I) \leftrightarrow (F \approx (i \cup \{q\}) \land (i \cup \{q\}) \cup H \in I))$
111	110	rspcev	$⊢ (i \cup \{q\} \in 𝒫 G \land (F \approx (i \cup \{q\}) \land (i \cup \{q\}) \cup H \in I)) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
112	87 100 106 111	syl12anc	$⊢ (((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \land (i \in 𝒫 (G ∖ \{q\}) \land ((F ∖ \{r\}) \approx i \land i \cup (H \cup \{q\}) \in I))) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
113	76 112	rexlimddv	$⊢ ((φ \land r \in F) \land (q \in G \land \neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
114	31 113	sylan2br	$⊢ ((φ \land r \in F) \land (q \in G \land (\neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I))) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
115	30 114	rexlimddv	$⊢ (φ \land r \in F) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
116	115	adantlr	$⊢ ((φ \land F \neq \emptyset) \land r \in F) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
117	22 116	exlimddv	$⊢ (φ \land F \neq \emptyset) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
118	19 117	pm2.61dane	$⊢ φ \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$

Metamath Proof Explorer

Theorem mreexexlem4d

Proof