mreexexd

Description: Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if F and G are disjoint from H , ( F u. H ) is independent, F is contained in the closure of ( G u. H ) , and either F or G is finite, then there is a subset q of G equinumerous to F such that ( q u. H ) is independent. This implies the case of Proposition 4.2.1 in FaureFrolicher p. 86 where either ( A \ B ) or ( B \ A ) is finite. The theorem is proven by induction using mreexexlem3d for the base case and mreexexlem4d for the induction step. (Contributed by David Moews, 1-May-2017) Remove dependencies on ax-rep and ax-ac2 . (Revised by Brendan Leahy, 2-Jun-2021)

	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$
	mreexexd.9	$⊢ φ \to (F \in Fin \lor G \in Fin)$
Assertion	mreexexd	$⊢ φ \to \exists q \in 𝒫 G (F \approx q \land q \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		mreexexd.9	$⊢ φ \to (F \in Fin \lor G \in Fin)$
10	1	elfvexd	$⊢ φ \to X \in V$
11		exmid	$⊢ (F \in Fin \lor \neg F \in Fin)$
12		ficardid	$⊢ F \in Fin \to card (F) \approx F$
13	12	ensymd	$⊢ F \in Fin \to F \approx card (F)$
14		iftrue	$⊢ F \in Fin \to if (F \in Fin, card (F), card (G)) = card (F)$
15	13 14	breqtrrd	$⊢ F \in Fin \to F \approx if (F \in Fin, card (F), card (G))$
16	15	a1i	$⊢ φ \to (F \in Fin \to F \approx if (F \in Fin, card (F), card (G)))$
17	9	orcanai	$⊢ (φ \land \neg F \in Fin) \to G \in Fin$
18		ficardid	$⊢ G \in Fin \to card (G) \approx G$
19	18	ensymd	$⊢ G \in Fin \to G \approx card (G)$
20	17 19	syl	$⊢ (φ \land \neg F \in Fin) \to G \approx card (G)$
21		iffalse	$⊢ \neg F \in Fin \to if (F \in Fin, card (F), card (G)) = card (G)$
22	21	adantl	$⊢ (φ \land \neg F \in Fin) \to if (F \in Fin, card (F), card (G)) = card (G)$
23	20 22	breqtrrd	$⊢ (φ \land \neg F \in Fin) \to G \approx if (F \in Fin, card (F), card (G))$
24	23	ex	$⊢ φ \to (\neg F \in Fin \to G \approx if (F \in Fin, card (F), card (G)))$
25	16 24	orim12d	$⊢ φ \to ((F \in Fin \lor \neg F \in Fin) \to (F \approx if (F \in Fin, card (F), card (G)) \lor G \approx if (F \in Fin, card (F), card (G))))$
26	11 25	mpi	$⊢ φ \to (F \approx if (F \in Fin, card (F), card (G)) \lor G \approx if (F \in Fin, card (F), card (G)))$
27		ficardom	$⊢ F \in Fin \to card (F) \in ω$
28	27	adantl	$⊢ (φ \land F \in Fin) \to card (F) \in ω$
29		ficardom	$⊢ G \in Fin \to card (G) \in ω$
30	17 29	syl	$⊢ (φ \land \neg F \in Fin) \to card (G) \in ω$
31	28 30	ifclda	$⊢ φ \to if (F \in Fin, card (F), card (G)) \in ω$
32		breq2	$⊢ l = \emptyset \to (f \approx l \leftrightarrow f \approx \emptyset)$
33		breq2	$⊢ l = \emptyset \to (g \approx l \leftrightarrow g \approx \emptyset)$
34	32 33	orbi12d	$⊢ l = \emptyset \to ((f \approx l \lor g \approx l) \leftrightarrow (f \approx \emptyset \lor g \approx \emptyset))$
35	34	3anbi1d	$⊢ l = \emptyset \to (((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \leftrightarrow ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I))$
36	35	imbi1d	$⊢ l = \emptyset \to ((((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow (((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
37	36	2ralbidv	$⊢ l = \emptyset \to (\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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
38	37	albidv	$⊢ l = \emptyset \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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
39	38	imbi2d	$⊢ l = \emptyset \to ((φ \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 i \in 𝒫 g (f \approx i \land i \cup h \in I))) \leftrightarrow (φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))))$
40		breq2	$⊢ l = k \to (f \approx l \leftrightarrow f \approx k)$
41		breq2	$⊢ l = k \to (g \approx l \leftrightarrow g \approx k)$
42	40 41	orbi12d	$⊢ l = k \to ((f \approx l \lor g \approx l) \leftrightarrow (f \approx k \lor g \approx k))$
43	42	3anbi1d	$⊢ l = k \to (((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \leftrightarrow ((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I))$
44	43	imbi1d	$⊢ l = k \to ((((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
45	44	2ralbidv	$⊢ l = k \to (\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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
46	45	albidv	$⊢ l = k \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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
47	46	imbi2d	$⊢ l = k \to ((φ \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 i \in 𝒫 g (f \approx i \land i \cup h \in I))) \leftrightarrow (φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))))$
48		breq2	$⊢ l = suc k \to (f \approx l \leftrightarrow f \approx suc k)$
49		breq2	$⊢ l = suc k \to (g \approx l \leftrightarrow g \approx suc k)$
50	48 49	orbi12d	$⊢ l = suc k \to ((f \approx l \lor g \approx l) \leftrightarrow (f \approx suc k \lor g \approx suc k))$
51	50	3anbi1d	$⊢ l = suc k \to (((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \leftrightarrow ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I))$
52	51	imbi1d	$⊢ l = suc k \to ((((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
53	52	2ralbidv	$⊢ l = suc k \to (\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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
54	53	albidv	$⊢ l = suc k \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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
55	54	imbi2d	$⊢ l = suc k \to ((φ \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 i \in 𝒫 g (f \approx i \land i \cup h \in I))) \leftrightarrow (φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))))$
56		breq2	$⊢ l = if (F \in Fin, card (F), card (G)) \to (f \approx l \leftrightarrow f \approx if (F \in Fin, card (F), card (G)))$
57		breq2	$⊢ l = if (F \in Fin, card (F), card (G)) \to (g \approx l \leftrightarrow g \approx if (F \in Fin, card (F), card (G)))$
58	56 57	orbi12d	$⊢ l = if (F \in Fin, card (F), card (G)) \to ((f \approx l \lor g \approx l) \leftrightarrow (f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))))$
59	58	3anbi1d	$⊢ l = if (F \in Fin, card (F), card (G)) \to (((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \leftrightarrow ((f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))) \land f \subseteq N (g \cup h) \land f \cup h \in I))$
60	59	imbi1d	$⊢ l = if (F \in Fin, card (F), card (G)) \to ((((f \approx l \lor g \approx l) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow (((f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
61	60	2ralbidv	$⊢ l = if (F \in Fin, card (F), card (G)) \to (\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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
62	61	albidv	$⊢ l = if (F \in Fin, card (F), card (G)) \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 i \in 𝒫 g (f \approx i \land i \cup h \in I)) \leftrightarrow \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
63	62	imbi2d	$⊢ l = if (F \in Fin, card (F), card (G)) \to ((φ \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 i \in 𝒫 g (f \approx i \land i \cup h \in I))) \leftrightarrow (φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))))$
64	1	ad2antrr	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to A \in Moore (X)$
65	4	ad2antrr	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
66		simplrl	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \in 𝒫 (X ∖ h)$
67	66	elpwid	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \subseteq X ∖ h$
68		simplrr	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to g \in 𝒫 (X ∖ h)$
69	68	elpwid	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to g \subseteq X ∖ h$
70		simpr2	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \subseteq N (g \cup h)$
71		simpr3	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \cup h \in I$
72		simpr1	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to (f \approx \emptyset \lor g \approx \emptyset)$
73		en0	$⊢ f \approx \emptyset \leftrightarrow f = \emptyset$
74		en0	$⊢ g \approx \emptyset \leftrightarrow g = \emptyset$
75	73 74	orbi12i	$⊢ (f \approx \emptyset \lor g \approx \emptyset) \leftrightarrow (f = \emptyset \lor g = \emptyset)$
76	72 75	sylib	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to (f = \emptyset \lor g = \emptyset)$
77	64 2 3 65 67 69 70 71 76	mreexexlem3d	$⊢ ((φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)$
78	77	ex	$⊢ (φ \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \to (((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
79	78	ralrimivva	$⊢ φ \to \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
80	79	alrimiv	$⊢ φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx \emptyset \lor g \approx \emptyset) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
81		nfv	$⊢ Ⅎ h φ$
82		nfv	$⊢ Ⅎ h k \in ω$
83		nfa1	$⊢ Ⅎ h \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
84	81 82 83	nf3an	$⊢ Ⅎ h (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
85		nfv	$⊢ Ⅎ f φ$
86		nfv	$⊢ Ⅎ f k \in ω$
87		nfra1	$⊢ Ⅎ f \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
88	87	nfal	$⊢ Ⅎ f \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
89	85 86 88	nf3an	$⊢ Ⅎ f (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
90		nfv	$⊢ Ⅎ g φ$
91		nfv	$⊢ Ⅎ g k \in ω$
92		nfra2w	$⊢ Ⅎ g \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
93	92	nfal	$⊢ Ⅎ g \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
94	90 91 93	nf3an	$⊢ Ⅎ g (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
95		nfv	$⊢ Ⅎ g f \in 𝒫 (X ∖ h)$
96	94 95	nfan	$⊢ Ⅎ g ((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land f \in 𝒫 (X ∖ h))$
97	1	3ad2ant1	$⊢ (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \to A \in Moore (X)$
98	97	ad2antrr	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to A \in Moore (X)$
99	4	3ad2ant1	$⊢ (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
100	99	ad2antrr	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
101		simplrl	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \in 𝒫 (X ∖ h)$
102	101	elpwid	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \subseteq X ∖ h$
103		simplrr	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to g \in 𝒫 (X ∖ h)$
104	103	elpwid	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to g \subseteq X ∖ h$
105		simpr2	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \subseteq N (g \cup h)$
106		simpr3	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to f \cup h \in I$
107		simpll2	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to k \in ω$
108		simpll3	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
109		simpr1	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to (f \approx suc k \lor g \approx suc k)$
110	98 2 3 100 102 104 105 106 107 108 109	mreexexlem4d	$⊢ (((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \land ((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I)) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)$
111	110	ex	$⊢ ((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land (f \in 𝒫 (X ∖ h) \land g \in 𝒫 (X ∖ h))) \to (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
112	111	expr	$⊢ ((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land f \in 𝒫 (X ∖ h)) \to (g \in 𝒫 (X ∖ h) \to (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
113	96 112	ralrimi	$⊢ ((φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \land f \in 𝒫 (X ∖ h)) \to \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
114	113	ex	$⊢ (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \to (f \in 𝒫 (X ∖ h) \to \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
115	89 114	ralrimi	$⊢ (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \to \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
116	84 115	alrimi	$⊢ (φ \land k \in ω \land \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
117	116	3exp	$⊢ φ \to (k \in ω \to (\forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)) \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))))$
118	117	com12	$⊢ k \in ω \to (φ \to (\forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)) \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))))$
119	118	a2d	$⊢ k \in ω \to ((φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx k \lor g \approx k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))) \to (φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx suc k \lor g \approx suc k) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))))$
120	39 47 55 63 80 119	finds	$⊢ if (F \in Fin, card (F), card (G)) \in ω \to (φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I)))$
121	31 120	mpcom	$⊢ φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx if (F \in Fin, card (F), card (G)) \lor g \approx if (F \in Fin, card (F), card (G))) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists i \in 𝒫 g (f \approx i \land i \cup h \in I))$
122	10 5 6 7 8 26 121	mreexexlemd	$⊢ φ \to \exists q \in 𝒫 G (F \approx q \land q \cup H \in I)$

Metamath Proof Explorer

Theorem mreexexd

Proof