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	bilani	$⊢ (φ \land F \neq \emptyset) \to \exists r r \in F$
22	1	adantr	$⊢ (φ \land r \in F) \to A \in Moore (X)$
23	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\})$
24	5	adantr	$⊢ (φ \land r \in F) \to F \subseteq X ∖ H$
25	6	adantr	$⊢ (φ \land r \in F) \to G \subseteq X ∖ H$
26	7	adantr	$⊢ (φ \land r \in F) \to F \subseteq N (G \cup H)$
27	8	adantr	$⊢ (φ \land r \in F) \to F \cup H \in I$
28		simpr	$⊢ (φ \land r \in F) \to r \in F$
29	22 2 3 23 24 25 26 27 28	mreexexlem2d	$⊢ (φ \land r \in F) \to \exists q \in G (\neg q \in (F ∖ \{r\}) \land (F ∖ \{r\}) \cup (H \cup \{q\}) \in I)$
30		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))$
31	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)$
32	31	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$
33		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\})$
34		difsnb	$⊢ \neg q \in (F ∖ \{r\}) \leftrightarrow (F ∖ \{r\}) ∖ \{q\} = F ∖ \{r\}$
35	33 34	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\}$
36	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$
37	36	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$
38	37	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\}$
39	35 38	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\}$
40		difun1	$⊢ X ∖ (H \cup \{q\}) = (X ∖ H) ∖ \{q\}$
41	39 40	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\})$
42	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$
43	42	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\}$
44	43 40	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\})$
45	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)$
46		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$
47		uncom	$⊢ H \cup \{q\} = \{q\} \cup H$
48	47	uneq2i	$⊢ (G ∖ \{q\}) \cup (H \cup \{q\}) = (G ∖ \{q\}) \cup (\{q\} \cup H)$
49		unass	$⊢ ((G ∖ \{q\}) \cup \{q\}) \cup H = (G ∖ \{q\}) \cup (\{q\} \cup H)$
50		difsnid	$⊢ q \in G \to (G ∖ \{q\}) \cup \{q\} = G$
51	50	uneq1d	$⊢ q \in G \to ((G ∖ \{q\}) \cup \{q\}) \cup H = G \cup H$
52	49 51	eqtr3id	$⊢ q \in G \to (G ∖ \{q\}) \cup (\{q\} \cup H) = G \cup H$
53	48 52	eqtrid	$⊢ q \in G \to (G ∖ \{q\}) \cup (H \cup \{q\}) = G \cup H$
54	46 53	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$
55	54	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)$
56	45 55	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\}))$
57	56	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\}))$
58		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$
59	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)$
60	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 ω$
61		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$
62		3anan12	$⊢ (L \in ω \land F \approx suc L \land r \in F) \leftrightarrow (F \approx suc L \land (L \in ω \land r \in F))$
63		dif1ennn	$⊢ (L \in ω \land F \approx suc L \land r \in F) \to (F ∖ \{r\}) \approx L$
64	62 63	sylbir	$⊢ (F \approx suc L \land (L \in ω \land r \in F)) \to (F ∖ \{r\}) \approx L$
65	64	expcom	$⊢ (L \in ω \land r \in F) \to (F \approx suc L \to (F ∖ \{r\}) \approx L)$
66	60 61 65	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)$
67		3anan12	$⊢ (L \in ω \land G \approx suc L \land q \in G) \leftrightarrow (G \approx suc L \land (L \in ω \land q \in G))$
68		dif1ennn	$⊢ (L \in ω \land G \approx suc L \land q \in G) \to (G ∖ \{q\}) \approx L$
69	67 68	sylbir	$⊢ (G \approx suc L \land (L \in ω \land q \in G)) \to (G ∖ \{q\}) \approx L$
70	69	expcom	$⊢ (L \in ω \land q \in G) \to (G \approx suc L \to (G ∖ \{q\}) \approx L)$
71	60 46 70	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)$
72	66 71	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))$
73	59 72	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)$
74	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))$
75	32 41 44 57 58 73 74	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)$
76	32	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$
77	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$
78	77	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$
79	76 78	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$
80		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\})$
81	80	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\}$
82	81	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$
83		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$
84	83	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$
85	82 84	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$
86	79 85	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$
87		difsnid	$⊢ r \in F \to (F ∖ \{r\}) \cup \{r\} = F$
88	87	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$
89		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$
90		en2sn	$⊢ (r \in V \land q \in V) \to \{r\} \approx \{q\}$
91	90	el2v	$⊢ \{r\} \approx \{q\}$
92	91	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\}$
93		disjdifr	$⊢ (F ∖ \{r\}) \cap \{r\} = \emptyset$
94	93	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$
95		ssdifin0	$⊢ i \subseteq G ∖ \{q\} \to i \cap \{q\} = \emptyset$
96	81 95	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$
97		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\})$
98	89 92 94 96 97	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\})$
99	88 98	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\})$
100		unass	$⊢ (i \cup \{q\}) \cup H = i \cup (\{q\} \cup H)$
101		uncom	$⊢ \{q\} \cup H = H \cup \{q\}$
102	101	uneq2i	$⊢ i \cup (\{q\} \cup H) = i \cup (H \cup \{q\})$
103	100 102	eqtr2i	$⊢ i \cup (H \cup \{q\}) = (i \cup \{q\}) \cup H$
104		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$
105	103 104	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$
106		breq2	$⊢ j = i \cup \{q\} \to (F \approx j \leftrightarrow F \approx (i \cup \{q\}))$
107		uneq1	$⊢ j = i \cup \{q\} \to j \cup H = (i \cup \{q\}) \cup H$
108	107	eleq1d	$⊢ j = i \cup \{q\} \to (j \cup H \in I \leftrightarrow (i \cup \{q\}) \cup H \in I)$
109	106 108	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))$
110	109	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)$
111	86 99 105 110	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)$
112	75 111	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)$
113	30 112	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)$
114	29 113	rexlimddv	$⊢ (φ \land r \in F) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
115	114	adantlr	$⊢ ((φ \land F \neq \emptyset) \land r \in F) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
116	21 115	exlimddv	$⊢ (φ \land F \neq \emptyset) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
117	19 116	pm2.61dane	$⊢ φ \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$

Metamath Proof Explorer

Theorem mreexexlem4d

Proof