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	syl5eqr	$⊢ q \in G \to (G ∖ \{q\}) \cup (\{q\} \cup H) = G \cup H$
54	49 53	syl5eq	$⊢ 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		incom	$⊢ (F ∖ \{r\}) \cap \{r\} = \{r\} \cap (F ∖ \{r\})$
95		disjdif	$⊢ \{r\} \cap (F ∖ \{r\}) = \emptyset$
96	94 95	eqtri	$⊢ (F ∖ \{r\}) \cap \{r\} = \emptyset$
97	96	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$
98		ssdifin0	$⊢ i \subseteq G ∖ \{q\} \to i \cap \{q\} = \emptyset$
99	82 98	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$
100		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\})$
101	90 93 97 99 100	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\})$
102	89 101	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\})$
103		unass	$⊢ (i \cup \{q\}) \cup H = i \cup (\{q\} \cup H)$
104		uncom	$⊢ \{q\} \cup H = H \cup \{q\}$
105	104	uneq2i	$⊢ i \cup (\{q\} \cup H) = i \cup (H \cup \{q\})$
106	103 105	eqtr2i	$⊢ i \cup (H \cup \{q\}) = (i \cup \{q\}) \cup H$
107		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$
108	106 107	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$
109		breq2	$⊢ j = i \cup \{q\} \to (F \approx j \leftrightarrow F \approx (i \cup \{q\}))$
110		uneq1	$⊢ j = i \cup \{q\} \to j \cup H = (i \cup \{q\}) \cup H$
111	110	eleq1d	$⊢ j = i \cup \{q\} \to (j \cup H \in I \leftrightarrow (i \cup \{q\}) \cup H \in I)$
112	109 111	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))$
113	112	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)$
114	87 102 108 113	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)$
115	76 114	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)$
116	31 115	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)$
117	30 116	rexlimddv	$⊢ (φ \land r \in F) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
118	117	adantlr	$⊢ ((φ \land F \neq \emptyset) \land r \in F) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
119	22 118	exlimddv	$⊢ (φ \land F \neq \emptyset) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$
120	19 119	pm2.61dane	$⊢ φ \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$

Metamath Proof Explorer

Theorem mreexexlem4d

Proof