Theorem mreexexd 17706

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 17704 for the base case and mreexexlem4d 17705 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5303 and ax-ac2 10532. (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 6959	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
3		mreexexlem2d.5	. 2 ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))
4		mreexexlem2d.6	. 2 ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))
5		mreexexlem2d.7	. 2 ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))
6		mreexexlem2d.8	. 2 ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)
7		exmid 893	. . 3 ⊢ (𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin)
8		ficardid 10031	. . . . . . 7 ⊢ (𝐹 ∈ Fin → (card‘𝐹) ≈ 𝐹)
9	8	ensymd 9065	. . . . . 6 ⊢ (𝐹 ∈ Fin → 𝐹 ≈ (card‘𝐹))
10		iftrue 4554	. . . . . 6 ⊢ (𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐹))
11	9, 10	breqtrrd 5194	. . . . 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 1003	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ∈ Fin)
15		ficardid 10031	. . . . . . . 8 ⊢ (𝐺 ∈ Fin → (card‘𝐺) ≈ 𝐺)
16	15	ensymd 9065	. . . . . . 7 ⊢ (𝐺 ∈ Fin → 𝐺 ≈ (card‘𝐺))
17	14, 16	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ (card‘𝐺))
18		iffalse 4557	. . . . . . 7 ⊢ (¬ 𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
19	18	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
20	17, 19	breqtrrd 5194	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
21	20	ex 412	. . . 4 ⊢ (𝜑 → (¬ 𝐹 ∈ Fin → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
22	12, 21	orim12d 965	. . 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 10030	. . . . 5 ⊢ (𝐹 ∈ Fin → (card‘𝐹) ∈ ω)
25	24	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ Fin) → (card‘𝐹) ∈ ω)
26		ficardom 10030	. . . . 5 ⊢ (𝐺 ∈ Fin → (card‘𝐺) ∈ ω)
27	14, 26	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → (card‘𝐺) ∈ ω)
28	25, 27	ifclda 4583	. . 3 ⊢ (𝜑 → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∈ ω)
29		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = ∅ → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ ∅))
30		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = ∅ → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ ∅))
31	29, 30	orbi12d 917	. . . . . . . . 9 ⊢ (𝑙 = ∅ → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅)))
32	31	3anbi1d 1440	. . . . . . . 8 ⊢ (𝑙 = ∅ → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
33	32	imbi1d 341	. . . . . . 7 ⊢ (𝑙 = ∅ → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
34	33	2ralbidv 3227	. . . . . 6 ⊢ (𝑙 = ∅ → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
35	34	albidv 1919	. . . . 5 ⊢ (𝑙 = ∅ → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
36	35	imbi2d 340	. . . 4 ⊢ (𝑙 = ∅ → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
37		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = 𝑘 → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ 𝑘))
38		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = 𝑘 → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ 𝑘))
39	37, 38	orbi12d 917	. . . . . . . . 9 ⊢ (𝑙 = 𝑘 → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘)))
40	39	3anbi1d 1440	. . . . . . . 8 ⊢ (𝑙 = 𝑘 → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
41	40	imbi1d 341	. . . . . . 7 ⊢ (𝑙 = 𝑘 → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
42	41	2ralbidv 3227	. . . . . 6 ⊢ (𝑙 = 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
43	42	albidv 1919	. . . . 5 ⊢ (𝑙 = 𝑘 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
44	43	imbi2d 340	. . . 4 ⊢ (𝑙 = 𝑘 → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
45		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = suc 𝑘 → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ suc 𝑘))
46		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = suc 𝑘 → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ suc 𝑘))
47	45, 46	orbi12d 917	. . . . . . . . 9 ⊢ (𝑙 = suc 𝑘 → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘)))
48	47	3anbi1d 1440	. . . . . . . 8 ⊢ (𝑙 = suc 𝑘 → (((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) ↔ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)))
49	48	imbi1d 341	. . . . . . 7 ⊢ (𝑙 = suc 𝑘 → ((((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
50	49	2ralbidv 3227	. . . . . 6 ⊢ (𝑙 = suc 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
51	50	albidv 1919	. . . . 5 ⊢ (𝑙 = suc 𝑘 → (∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
52	51	imbi2d 340	. . . 4 ⊢ (𝑙 = suc 𝑘 → ((𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ↔ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))))
53		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑓 ≈ 𝑙 ↔ 𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
54		breq2 5170	. . . . . . . . . 10 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑔 ≈ 𝑙 ↔ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
55	53, 54	orbi12d 917	. . . . . . . . 9 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ↔ (𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))))
56	55	3anbi1d 1440	. . . . . . . 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 3227	. . . . . 6 ⊢ (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
59	58	albidv 1919	. . . . 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 725	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
62		mreexexlem2d.2	. . . . . . . 8 ⊢ 𝑁 = (mrCls‘𝐴)
63		mreexexlem2d.3	. . . . . . . 8 ⊢ 𝐼 = (mrInd‘𝐴)
64		mreexexlem2d.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
65	64	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
66		simplrl 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
67	66	elpwid 4631	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑋 ∖ ℎ))
68		simplrr 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))
69	68	elpwid 4631	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ⊆ (𝑋 ∖ ℎ))
70		simpr2 1195	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)))
71		simpr3 1196	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ∪ ℎ) ∈ 𝐼)
72		simpr1 1194	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅))
73		en0 9078	. . . . . . . . . 10 ⊢ (𝑓 ≈ ∅ ↔ 𝑓 = ∅)
74		en0 9078	. . . . . . . . . 10 ⊢ (𝑔 ≈ ∅ ↔ 𝑔 = ∅)
75	73, 74	orbi12i 913	. . . . . . . . 9 ⊢ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ↔ (𝑓 = ∅ ∨ 𝑔 = ∅))
76	72, 75	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 = ∅ ∨ 𝑔 = ∅))
77	61, 62, 63, 65, 67, 69, 70, 71, 76	mreexexlem3d 17704	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
78	77	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) → (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
79	78	ralrimivva 3208	. . . . 5 ⊢ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
80	79	alrimiv 1926	. . . 4 ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
81		nfv 1913	. . . . . . . . 9 ⊢ Ⅎℎ𝜑
82		nfv 1913	. . . . . . . . 9 ⊢ Ⅎℎ 𝑘 ∈ ω
83		nfa1 2152	. . . . . . . . 9 ⊢ Ⅎℎ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
84	81, 82, 83	nf3an 1900	. . . . . . . 8 ⊢ Ⅎℎ(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
85		nfv 1913	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜑
86		nfv 1913	. . . . . . . . . 10 ⊢ Ⅎ𝑓 𝑘 ∈ ω
87		nfra1 3290	. . . . . . . . . . 11 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
88	87	nfal 2327	. . . . . . . . . 10 ⊢ Ⅎ𝑓∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
89	85, 86, 88	nf3an 1900	. . . . . . . . 9 ⊢ Ⅎ𝑓(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
90		nfv 1913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔𝜑
91		nfv 1913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔 𝑘 ∈ ω
92		nfra2w 3305	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
93	92	nfal 2327	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
94	90, 91, 93	nf3an 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔(𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
95		nfv 1913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)
96	94, 95	nfan 1898	. . . . . . . . . . 11 ⊢ Ⅎ𝑔((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
97	1	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → 𝐴 ∈ (Moore‘𝑋))
98	97	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
99	64	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
100	99	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
101		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ))
102	101	elpwid 4631	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑋 ∖ ℎ))
103		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))
104	103	elpwid 4631	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑔 ⊆ (𝑋 ∖ ℎ))
105		simpr2 1195	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)))
106		simpr3 1196	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ∪ ℎ) ∈ 𝐼)
107		simpll2 1213	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → 𝑘 ∈ ω)
108		simpll3 1214	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
109		simpr1 1194	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → (𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘))
110	98, 62, 63, 100, 102, 104, 105, 106, 107, 108, 109	mreexexlem4d 17705	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) ∧ ((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))
111	110	ex 412	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) ∧ 𝑔 ∈ 𝒫 (𝑋 ∖ ℎ))) → (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
112	111	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)) → (𝑔 ∈ 𝒫 (𝑋 ∖ ℎ) → (((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
113	96, 112	ralrimi 3263	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)) → ∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼)))
114	113	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ω ∧ ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))) → (𝑓 ∈ 𝒫 (𝑋 ∖ ℎ) → ∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓 ≈ 𝑖 ∧ (𝑖 ∪ ℎ) ∈ 𝐼))))
115	89, 114	ralrimi 3263	. . . . . . . 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 7936	. . 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 17702	1 ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 846   ∧ w3a 1087  ∀wal 1535   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ⊆ wss 3976  ∅c0 4352  ifcif 4548  𝒫 cpw 4622  {csn 4648   class class class wbr 5166  suc csuc 6397  ‘cfv 6573  ωcom 7903   ≈ cen 9000  Fincfn 9003  cardccrd 10004  Moorecmre 17640  mrClscmrc 17641  mrIndcmri 17642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-om 7904  df-1o 8522  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-card 10008  df-mre 17644  df-mrc 17645  df-mri 17646

This theorem is referenced by:  mreexdomd  17707  lindsdom  37574  aacllem  48895