Theorem mreexexd 17609

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 17607 for the base case and mreexexlem4d 17608 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5202 and ax-ac2 10380. (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 6867	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
3		mreexexlem2d.5	. 2 ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))
4		mreexexlem2d.6	. 2 ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))
5		mreexexlem2d.7	. 2 ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))
6		mreexexlem2d.8	. 2 ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)
7		exmid 901	. . 3 ⊢ (𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin)
8		ficardid 9881	. . . . . . 7 ⊢ (𝐹 ∈ Fin → (card‘𝐹) ≈ 𝐹)
9	8	ensymd 8946	. . . . . 6 ⊢ (𝐹 ∈ Fin → 𝐹 ≈ (card‘𝐹))
10		iftrue 4463	. . . . . 6 ⊢ (𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐹))
11	9, 10	breqtrrd 5103	. . . . 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 1011	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ∈ Fin)
15		ficardid 9881	. . . . . . . 8 ⊢ (𝐺 ∈ Fin → (card‘𝐺) ≈ 𝐺)
16	15	ensymd 8946	. . . . . . 7 ⊢ (𝐺 ∈ Fin → 𝐺 ≈ (card‘𝐺))
17	14, 16	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ (card‘𝐺))
18		iffalse 4466	. . . . . . 7 ⊢ (¬ 𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
19	18	adantl 483	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
20	17, 19	breqtrrd 5103	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
21	20	ex 414	. . . 4 ⊢ (𝜑 → (¬ 𝐹 ∈ Fin → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
22	12, 21	orim12d 973	. . 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 9880	. . . . 5 ⊢ (𝐹 ∈ Fin → (card‘𝐹) ∈ ω)
25	24	adantl 483	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ Fin) → (card‘𝐹) ∈ ω)
26		ficardom 9880	. . . . 5 ⊢ (𝐺 ∈ Fin → (card‘𝐺) ∈ ω)
27	14, 26	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → (card‘𝐺) ∈ ω)
28	25, 27	ifclda 4493	. . 3 ⊢ (𝜑 → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∈ ω)
29		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = ∅ → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ ∅))
30		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = ∅ → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ ∅))
31	29, 30	orbi12d 925	. . . . . . . . 9 ⊢ (𝑙 = ∅ → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅)))
32	31	3anbi1d 1449	. . . . . . . 8 ⊢ (𝑙 = ∅ → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
33	32	imbi1d 343	. . . . . . 7 ⊢ (𝑙 = ∅ → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
34	33	2ralbidv 3205	. . . . . 6 ⊢ (𝑙 = ∅ → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
35	34	albidv 1928	. . . . 5 ⊢ (𝑙 = ∅ → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
36	35	imbi2d 342	. . . 4 ⊢ (𝑙 = ∅ → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
37		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = 𝑘 → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ 𝑘))
38		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = 𝑘 → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ 𝑘))
39	37, 38	orbi12d 925	. . . . . . . . 9 ⊢ (𝑙 = 𝑘 → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘)))
40	39	3anbi1d 1449	. . . . . . . 8 ⊢ (𝑙 = 𝑘 → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
41	40	imbi1d 343	. . . . . . 7 ⊢ (𝑙 = 𝑘 → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
42	41	2ralbidv 3205	. . . . . 6 ⊢ (𝑙 = 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
43	42	albidv 1928	. . . . 5 ⊢ (𝑙 = 𝑘 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
44	43	imbi2d 342	. . . 4 ⊢ (𝑙 = 𝑘 → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
45		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = suc 𝑘 → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ suc 𝑘))
46		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = suc 𝑘 → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ suc 𝑘))
47	45, 46	orbi12d 925	. . . . . . . . 9 ⊢ (𝑙 = suc 𝑘 → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘)))
48	47	3anbi1d 1449	. . . . . . . 8 ⊢ (𝑙 = suc 𝑘 → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
49	48	imbi1d 343	. . . . . . 7 ⊢ (𝑙 = suc 𝑘 → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
50	49	2ralbidv 3205	. . . . . 6 ⊢ (𝑙 = suc 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
51	50	albidv 1928	. . . . 5 ⊢ (𝑙 = suc 𝑘 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
52	51	imbi2d 342	. . . 4 ⊢ (𝑙 = suc 𝑘 → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
53		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
54		breq2 5079	. . . . . . . . . 10 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
55	53, 54	orbi12d 925	. . . . . . . . 9 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))))
56	55	3anbi1d 1449	. . . . . . . 8 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
57	56	imbi1d 343	. . . . . . 7 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
58	57	2ralbidv 3205	. . . . . 6 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
59	58	albidv 1928	. . . . 5 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
60	59	imbi2d 342	. . . 4 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
61	1	ad2antrr 733	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
62		mreexexlem2d.2	. . . . . . . 8 ⊢ 𝑁 = (mrCls‘𝐴)
63		mreexexlem2d.3	. . . . . . . 8 ⊢ 𝐼 = (mrInd‘𝐴)
64		mreexexlem2d.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
65	64	ad2antrr 733	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
66		simplrl 783	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
67	66	elpwid 4541	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑋 ∖ ℎ))
68		simplrr 784	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))
69	68	elpwid 4541	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ⊆ (𝑋 ∖ ℎ))
70		simpr2 1203	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)))
71		simpr3 1204	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ∪ ℎ) ∈ 𝐼)
72		simpr1 1202	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅))
73		en0 8959	. . . . . . . . . 10 ⊢ (𝑓 ≈ ∅ ↔ 𝑓 = ∅)
74		en0 8959	. . . . . . . . . 10 ⊢ (𝑔 ≈ ∅ ↔ 𝑔 = ∅)
75	73, 74	orbi12i 921	. . . . . . . . 9 ⊢ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ↔ (𝑓 = ∅ ∨ 𝑔 = ∅))
76	72, 75	sylib 220	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 = ∅ ∨ 𝑔 = ∅))
77	61, 62, 63, 65, 67, 69, 70, 71, 76	mreexexlem3d 17607	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
78	77	ex 414	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) → (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
79	78	ralrimivva 3184	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
80	79	alrimiv 1935	. . . 4 ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
81		nfv 1922	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
82		nfv 1922	. . . . . . . . 9 ⊢ Ⅎℎ 𝑘 ∈ ω
83		nfa1 2164	. . . . . . . . 9 ⊢ Ⅎℎ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
84	81, 82, 83	nf3an 1909	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
85		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜑
86		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑓 𝑘 ∈ ω
87		nfra1 3265	. . . . . . . . . . 11 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
88	87	nfal 2334	. . . . . . . . . 10 ⊢ Ⅎ𝑓∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
89	85, 86, 88	nf3an 1909	. . . . . . . . 9 ⊢ Ⅎ𝑓(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
90		nfv 1922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝜑
91		nfv 1922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔 𝑘 ∈ ω
92		nfra2w 3277	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
93	92	nfal 2334	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
94	90, 91, 93	nf3an 1909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
95		nfv 1922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)
96	94, 95	nfan 1907	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
97	1	3ad2ant1 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → 𝐴 ∈ (Moore‘𝑋))
98	97	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
99	64	3ad2ant1 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
100	99	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
101		simplrl 783	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
102	101	elpwid 4541	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑋 ∖ ℎ))
103		simplrr 784	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))
104	103	elpwid 4541	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ⊆ (𝑋 ∖ ℎ))
105		simpr2 1203	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)))
106		simpr3 1204	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ∪ ℎ) ∈ 𝐼)
107		simpll2 1221	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑘 ∈ ω)
108		simpll3 1222	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
109		simpr1 1202	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘))
110	98, 62, 63, 100, 102, 104, 105, 106, 107, 108, 109	mreexexlem4d 17608	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
111	110	ex 414	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) → (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
112	111	expr 458	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)) → (𝑔 ∈ 𝒫 (𝑋 ∖ ℎ) → (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
113	96, 112	ralrimi 3239	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)) → ∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
114	113	ex 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) → ∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
115	89, 114	ralrimi 3239	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
116	84, 115	alrimi 2227	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
117	116	3exp 1126	. . . . . 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 7840	. . 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 17605	1 ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 854   ∧ w3a 1093  ∀wal 1546   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ∃wrex 3065  Vcvv 3433   ∖ cdif 3882   ∪ cun 3883   ⊆ wss 3885  ∅c0 4264  ifcif 4457  𝒫 cpw 4532  {csn 4558   class class class wbr 5075  suc csuc 6316  ‘cfv 6489  ωcom 7810   ≈ cen 8884  Fincfn 8887  cardccrd 9854  Moorecmre 17539  mrClscmrc 17540  mrIndcmri 17541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-int 4881  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-om 7811  df-1o 8399  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-card 9858  df-mre 17543  df-mrc 17544  df-mri 17545

This theorem is referenced by:  mreexdomd  17610  lindsdom  37996  aacllem  50305