Theorem mreexexd 17585

Description: Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if 𝐹 and 𝐺 are disjoint from 𝐻, (𝐹 ∪ 𝐻) is independent, 𝐹 is contained in the closure of (𝐺 ∪ 𝐻), and either 𝐹 or 𝐺 is finite, then there is a subset 𝑞 of 𝐺 equinumerous to 𝐹 such that (𝑞 ∪ 𝐻) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either (𝐴 ∖ 𝐵) or (𝐵 ∖ 𝐴) is finite. The theorem is proven by induction using mreexexlem3d 17583 for the base case and mreexexlem4d 17584 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5229 and ax-ac2 10392. (Revised by Brendan Leahy, 2-Jun-2021.)

Hypotheses

Ref	Expression
mreexexlem2d.1	⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
mreexexlem2d.2	⊢ 𝑁 = (mrCls‘𝐴)
mreexexlem2d.3	⊢ 𝐼 = (mrInd‘𝐴)
mreexexlem2d.4	⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
mreexexlem2d.5	⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))
mreexexlem2d.6	⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))
mreexexlem2d.7	⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))
mreexexlem2d.8	⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)
mreexexd.9	⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))

Assertion

Ref	Expression
mreexexd	⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼))

Distinct variable groups:   𝐹,𝑞   𝐺,𝑞   𝑋,𝑠,𝑦,𝑧   𝜑,𝑠,𝑦,𝑧   𝐼,𝑠,𝑦,𝑧   𝑁,𝑠,𝑦,𝑧   𝜑,𝑞   𝐼,𝑞   𝐻,𝑞

Allowed substitution hints:   𝐴(𝑦,𝑧,𝑠,𝑞)   𝐹(𝑦,𝑧,𝑠)   𝐺(𝑦,𝑧,𝑠)   𝐻(𝑦,𝑧,𝑠)   𝑁(𝑞)   𝑋(𝑞)

Proof of Theorem mreexexd

Dummy variables 𝑓 𝑔 ℎ 𝑙 𝑘 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mreexexlem2d.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
2	1	elfvexd 6879	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
3		mreexexlem2d.5	. 2 ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))
4		mreexexlem2d.6	. 2 ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))
5		mreexexlem2d.7	. 2 ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))
6		mreexexlem2d.8	. 2 ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)
7		exmid 894	. . 3 ⊢ (𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin)
8		ficardid 9891	. . . . . . 7 ⊢ (𝐹 ∈ Fin → (card‘𝐹) ≈ 𝐹)
9	8	ensymd 8953	. . . . . 6 ⊢ (𝐹 ∈ Fin → 𝐹 ≈ (card‘𝐹))
10		iftrue 4490	. . . . . 6 ⊢ (𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐹))
11	9, 10	breqtrrd 5130	. . . . 5 ⊢ (𝐹 ∈ Fin → 𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
12	11	a1i 11	. . . 4 ⊢ (𝜑 → (𝐹 ∈ Fin → 𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
13		mreexexd.9	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))
14	13	orcanai 1004	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ∈ Fin)
15		ficardid 9891	. . . . . . . 8 ⊢ (𝐺 ∈ Fin → (card‘𝐺) ≈ 𝐺)
16	15	ensymd 8953	. . . . . . 7 ⊢ (𝐺 ∈ Fin → 𝐺 ≈ (card‘𝐺))
17	14, 16	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ (card‘𝐺))
18		iffalse 4493	. . . . . . 7 ⊢ (¬ 𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
19	18	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
20	17, 19	breqtrrd 5130	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
21	20	ex 412	. . . 4 ⊢ (𝜑 → (¬ 𝐹 ∈ Fin → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
22	12, 21	orim12d 966	. . 3 ⊢ (𝜑 → ((𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin) → (𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))))
23	7, 22	mpi 20	. 2 ⊢ (𝜑 → (𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
24		ficardom 9890	. . . . 5 ⊢ (𝐹 ∈ Fin → (card‘𝐹) ∈ ω)
25	24	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ Fin) → (card‘𝐹) ∈ ω)
26		ficardom 9890	. . . . 5 ⊢ (𝐺 ∈ Fin → (card‘𝐺) ∈ ω)
27	14, 26	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → (card‘𝐺) ∈ ω)
28	25, 27	ifclda 4520	. . 3 ⊢ (𝜑 → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∈ ω)
29		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = ∅ → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ ∅))
30		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = ∅ → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ ∅))
31	29, 30	orbi12d 918	. . . . . . . . 9 ⊢ (𝑙 = ∅ → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅)))
32	31	3anbi1d 1442	. . . . . . . 8 ⊢ (𝑙 = ∅ → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
33	32	imbi1d 341	. . . . . . 7 ⊢ (𝑙 = ∅ → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
34	33	2ralbidv 3199	. . . . . 6 ⊢ (𝑙 = ∅ → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
35	34	albidv 1920	. . . . 5 ⊢ (𝑙 = ∅ → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
36	35	imbi2d 340	. . . 4 ⊢ (𝑙 = ∅ → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
37		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = 𝑘 → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ 𝑘))
38		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = 𝑘 → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ 𝑘))
39	37, 38	orbi12d 918	. . . . . . . . 9 ⊢ (𝑙 = 𝑘 → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘)))
40	39	3anbi1d 1442	. . . . . . . 8 ⊢ (𝑙 = 𝑘 → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
41	40	imbi1d 341	. . . . . . 7 ⊢ (𝑙 = 𝑘 → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
42	41	2ralbidv 3199	. . . . . 6 ⊢ (𝑙 = 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
43	42	albidv 1920	. . . . 5 ⊢ (𝑙 = 𝑘 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
44	43	imbi2d 340	. . . 4 ⊢ (𝑙 = 𝑘 → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
45		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = suc 𝑘 → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ suc 𝑘))
46		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = suc 𝑘 → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ suc 𝑘))
47	45, 46	orbi12d 918	. . . . . . . . 9 ⊢ (𝑙 = suc 𝑘 → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘)))
48	47	3anbi1d 1442	. . . . . . . 8 ⊢ (𝑙 = suc 𝑘 → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
49	48	imbi1d 341	. . . . . . 7 ⊢ (𝑙 = suc 𝑘 → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
50	49	2ralbidv 3199	. . . . . 6 ⊢ (𝑙 = suc 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
51	50	albidv 1920	. . . . 5 ⊢ (𝑙 = suc 𝑘 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
52	51	imbi2d 340	. . . 4 ⊢ (𝑙 = suc 𝑘 → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
53		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
54		breq2 5106	. . . . . . . . . 10 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
55	53, 54	orbi12d 918	. . . . . . . . 9 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))))
56	55	3anbi1d 1442	. . . . . . . 8 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
57	56	imbi1d 341	. . . . . . 7 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
58	57	2ralbidv 3199	. . . . . 6 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
59	58	albidv 1920	. . . . 5 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
60	59	imbi2d 340	. . . 4 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
61	1	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
62		mreexexlem2d.2	. . . . . . . 8 ⊢ 𝑁 = (mrCls‘𝐴)
63		mreexexlem2d.3	. . . . . . . 8 ⊢ 𝐼 = (mrInd‘𝐴)
64		mreexexlem2d.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
65	64	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
66		simplrl 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
67	66	elpwid 4568	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑋 ∖ ℎ))
68		simplrr 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))
69	68	elpwid 4568	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ⊆ (𝑋 ∖ ℎ))
70		simpr2 1196	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)))
71		simpr3 1197	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ∪ ℎ) ∈ 𝐼)
72		simpr1 1195	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅))
73		en0 8966	. . . . . . . . . 10 ⊢ (𝑓 ≈ ∅ ↔ 𝑓 = ∅)
74		en0 8966	. . . . . . . . . 10 ⊢ (𝑔 ≈ ∅ ↔ 𝑔 = ∅)
75	73, 74	orbi12i 914	. . . . . . . . 9 ⊢ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ↔ (𝑓 = ∅ ∨ 𝑔 = ∅))
76	72, 75	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 = ∅ ∨ 𝑔 = ∅))
77	61, 62, 63, 65, 67, 69, 70, 71, 76	mreexexlem3d 17583	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
78	77	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) → (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
79	78	ralrimivva 3178	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
80	79	alrimiv 1927	. . . 4 ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
81		nfv 1914	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
82		nfv 1914	. . . . . . . . 9 ⊢ Ⅎℎ 𝑘 ∈ ω
83		nfa1 2152	. . . . . . . . 9 ⊢ Ⅎℎ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
84	81, 82, 83	nf3an 1901	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
85		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜑
86		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑓 𝑘 ∈ ω
87		nfra1 3259	. . . . . . . . . . 11 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
88	87	nfal 2322	. . . . . . . . . 10 ⊢ Ⅎ𝑓∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
89	85, 86, 88	nf3an 1901	. . . . . . . . 9 ⊢ Ⅎ𝑓(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
90		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝜑
91		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔 𝑘 ∈ ω
92		nfra2w 3272	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
93	92	nfal 2322	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
94	90, 91, 93	nf3an 1901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
95		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)
96	94, 95	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
97	1	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → 𝐴 ∈ (Moore‘𝑋))
98	97	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
99	64	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
100	99	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
101		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
102	101	elpwid 4568	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑋 ∖ ℎ))
103		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))
104	103	elpwid 4568	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ⊆ (𝑋 ∖ ℎ))
105		simpr2 1196	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)))
106		simpr3 1197	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ∪ ℎ) ∈ 𝐼)
107		simpll2 1214	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑘 ∈ ω)
108		simpll3 1215	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
109		simpr1 1195	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘))
110	98, 62, 63, 100, 102, 104, 105, 106, 107, 108, 109	mreexexlem4d 17584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
111	110	ex 412	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) → (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
112	111	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)) → (𝑔 ∈ 𝒫 (𝑋 ∖ ℎ) → (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
113	96, 112	ralrimi 3233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)) → ∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
114	113	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) → ∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
115	89, 114	ralrimi 3233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
116	84, 115	alrimi 2214	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
117	116	3exp 1119	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ω → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
118	117	com12 32	. . . . 5 ⊢ (𝑘 ∈ ω → (𝜑 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
119	118	a2d 29	. . . 4 ⊢ (𝑘 ∈ ω → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
120	36, 44, 52, 60, 80, 119	finds 7852	. . 3 ⊢ (if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∈ ω → (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
121	28, 120	mpcom 38	. 2 ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
122	2, 3, 4, 5, 6, 23, 121	mreexexlemd 17581	1 ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ⊆ wss 3911  ∅c0 4292  ifcif 4484  𝒫 cpw 4559  {csn 4585   class class class wbr 5102  suc csuc 6322  ‘cfv 6499  ωcom 7822   ≈ cen 8892  Fincfn 8895  cardccrd 9864  Moorecmre 17519  mrClscmrc 17520  mrIndcmri 17521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-om 7823  df-1o 8411  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-card 9868  df-mre 17523  df-mrc 17524  df-mri 17525

This theorem is referenced by:  mreexdomd  17586  lindsdom  37581  aacllem  49763