MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mreexexd Structured version   Visualization version   GIF version

Theorem mreexexd 17691
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 17689 for the base case and mreexexlem4d 17690 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5279 and ax-ac2 10503. (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.
StepHypRef Expression
1 mreexexlem2d.1 . . 3 (𝜑𝐴 ∈ (Moore‘𝑋))
21elfvexd 6945 . 2 (𝜑𝑋 ∈ V)
3 mreexexlem2d.5 . 2 (𝜑𝐹 ⊆ (𝑋𝐻))
4 mreexexlem2d.6 . 2 (𝜑𝐺 ⊆ (𝑋𝐻))
5 mreexexlem2d.7 . 2 (𝜑𝐹 ⊆ (𝑁‘(𝐺𝐻)))
6 mreexexlem2d.8 . 2 (𝜑 → (𝐹𝐻) ∈ 𝐼)
7 exmid 895 . . 3 (𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin)
8 ficardid 10002 . . . . . . 7 (𝐹 ∈ Fin → (card‘𝐹) ≈ 𝐹)
98ensymd 9045 . . . . . 6 (𝐹 ∈ Fin → 𝐹 ≈ (card‘𝐹))
10 iftrue 4531 . . . . . 6 (𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐹))
119, 10breqtrrd 5171 . . . . 5 (𝐹 ∈ Fin → 𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
1211a1i 11 . . . 4 (𝜑 → (𝐹 ∈ Fin → 𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
13 mreexexd.9 . . . . . . . 8 (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))
1413orcanai 1005 . . . . . . 7 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ∈ Fin)
15 ficardid 10002 . . . . . . . 8 (𝐺 ∈ Fin → (card‘𝐺) ≈ 𝐺)
1615ensymd 9045 . . . . . . 7 (𝐺 ∈ Fin → 𝐺 ≈ (card‘𝐺))
1714, 16syl 17 . . . . . 6 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ (card‘𝐺))
18 iffalse 4534 . . . . . . 7 𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
1918adantl 481 . . . . . 6 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
2017, 19breqtrrd 5171 . . . . 5 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
2120ex 412 . . . 4 (𝜑 → (¬ 𝐹 ∈ Fin → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
2212, 21orim12d 967 . . 3 (𝜑 → ((𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin) → (𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))))
237, 22mpi 20 . 2 (𝜑 → (𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
24 ficardom 10001 . . . . 5 (𝐹 ∈ Fin → (card‘𝐹) ∈ ω)
2524adantl 481 . . . 4 ((𝜑𝐹 ∈ Fin) → (card‘𝐹) ∈ ω)
26 ficardom 10001 . . . . 5 (𝐺 ∈ Fin → (card‘𝐺) ∈ ω)
2714, 26syl 17 . . . 4 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → (card‘𝐺) ∈ ω)
2825, 27ifclda 4561 . . 3 (𝜑 → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∈ ω)
29 breq2 5147 . . . . . . . . . 10 (𝑙 = ∅ → (𝑓𝑙𝑓 ≈ ∅))
30 breq2 5147 . . . . . . . . . 10 (𝑙 = ∅ → (𝑔𝑙𝑔 ≈ ∅))
3129, 30orbi12d 919 . . . . . . . . 9 (𝑙 = ∅ → ((𝑓𝑙𝑔𝑙) ↔ (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅)))
32313anbi1d 1442 . . . . . . . 8 (𝑙 = ∅ → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
3332imbi1d 341 . . . . . . 7 (𝑙 = ∅ → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
34332ralbidv 3221 . . . . . 6 (𝑙 = ∅ → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
3534albidv 1920 . . . . 5 (𝑙 = ∅ → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
3635imbi2d 340 . . . 4 (𝑙 = ∅ → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
37 breq2 5147 . . . . . . . . . 10 (𝑙 = 𝑘 → (𝑓𝑙𝑓𝑘))
38 breq2 5147 . . . . . . . . . 10 (𝑙 = 𝑘 → (𝑔𝑙𝑔𝑘))
3937, 38orbi12d 919 . . . . . . . . 9 (𝑙 = 𝑘 → ((𝑓𝑙𝑔𝑙) ↔ (𝑓𝑘𝑔𝑘)))
40393anbi1d 1442 . . . . . . . 8 (𝑙 = 𝑘 → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
4140imbi1d 341 . . . . . . 7 (𝑙 = 𝑘 → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
42412ralbidv 3221 . . . . . 6 (𝑙 = 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
4342albidv 1920 . . . . 5 (𝑙 = 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
4443imbi2d 340 . . . 4 (𝑙 = 𝑘 → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
45 breq2 5147 . . . . . . . . . 10 (𝑙 = suc 𝑘 → (𝑓𝑙𝑓 ≈ suc 𝑘))
46 breq2 5147 . . . . . . . . . 10 (𝑙 = suc 𝑘 → (𝑔𝑙𝑔 ≈ suc 𝑘))
4745, 46orbi12d 919 . . . . . . . . 9 (𝑙 = suc 𝑘 → ((𝑓𝑙𝑔𝑙) ↔ (𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘)))
48473anbi1d 1442 . . . . . . . 8 (𝑙 = suc 𝑘 → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
4948imbi1d 341 . . . . . . 7 (𝑙 = suc 𝑘 → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
50492ralbidv 3221 . . . . . 6 (𝑙 = suc 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
5150albidv 1920 . . . . 5 (𝑙 = suc 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
5251imbi2d 340 . . . 4 (𝑙 = suc 𝑘 → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
53 breq2 5147 . . . . . . . . . 10 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑓𝑙𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
54 breq2 5147 . . . . . . . . . 10 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑔𝑙𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
5553, 54orbi12d 919 . . . . . . . . 9 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝑓𝑙𝑔𝑙) ↔ (𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))))
56553anbi1d 1442 . . . . . . . 8 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
5756imbi1d 341 . . . . . . 7 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
58572ralbidv 3221 . . . . . 6 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
5958albidv 1920 . . . . 5 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
6059imbi2d 340 . . . 4 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
611ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
62 mreexexlem2d.2 . . . . . . . 8 𝑁 = (mrCls‘𝐴)
63 mreexexlem2d.3 . . . . . . . 8 𝐼 = (mrInd‘𝐴)
64 mreexexlem2d.4 . . . . . . . . 9 (𝜑 → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
6564ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
66 simplrl 777 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋))
6766elpwid 4609 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ⊆ (𝑋))
68 simplrr 778 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋))
6968elpwid 4609 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑔 ⊆ (𝑋))
70 simpr2 1196 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔)))
71 simpr3 1197 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓) ∈ 𝐼)
72 simpr1 1195 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅))
73 en0 9058 . . . . . . . . . 10 (𝑓 ≈ ∅ ↔ 𝑓 = ∅)
74 en0 9058 . . . . . . . . . 10 (𝑔 ≈ ∅ ↔ 𝑔 = ∅)
7573, 74orbi12i 915 . . . . . . . . 9 ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ↔ (𝑓 = ∅ ∨ 𝑔 = ∅))
7672, 75sylib 218 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓 = ∅ ∨ 𝑔 = ∅))
7761, 62, 63, 65, 67, 69, 70, 71, 76mreexexlem3d 17689 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
7877ex 412 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) → (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
7978ralrimivva 3202 . . . . 5 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
8079alrimiv 1927 . . . 4 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
81 nfv 1914 . . . . . . . . 9 𝜑
82 nfv 1914 . . . . . . . . 9 𝑘 ∈ ω
83 nfa1 2151 . . . . . . . . 9 𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
8481, 82, 83nf3an 1901 . . . . . . . 8 (𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
85 nfv 1914 . . . . . . . . . 10 𝑓𝜑
86 nfv 1914 . . . . . . . . . 10 𝑓 𝑘 ∈ ω
87 nfra1 3284 . . . . . . . . . . 11 𝑓𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
8887nfal 2323 . . . . . . . . . 10 𝑓𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
8985, 86, 88nf3an 1901 . . . . . . . . 9 𝑓(𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
90 nfv 1914 . . . . . . . . . . . . 13 𝑔𝜑
91 nfv 1914 . . . . . . . . . . . . 13 𝑔 𝑘 ∈ ω
92 nfra2w 3299 . . . . . . . . . . . . . 14 𝑔𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
9392nfal 2323 . . . . . . . . . . . . 13 𝑔𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
9490, 91, 93nf3an 1901 . . . . . . . . . . . 12 𝑔(𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
95 nfv 1914 . . . . . . . . . . . 12 𝑔 𝑓 ∈ 𝒫 (𝑋)
9694, 95nfan 1899 . . . . . . . . . . 11 𝑔((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋))
9713ad2ant1 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → 𝐴 ∈ (Moore‘𝑋))
9897ad2antrr 726 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
99643ad2ant1 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
10099ad2antrr 726 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
101 simplrl 777 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋))
102101elpwid 4609 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ⊆ (𝑋))
103 simplrr 778 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋))
104103elpwid 4609 . . . . . . . . . . . . . 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 𝑘))
11098, 62, 63, 100, 102, 104, 105, 106, 107, 108, 109mreexexlem4d 17690 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
111110ex 412 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) → (((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
112111expr 456 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋)) → (𝑔 ∈ 𝒫 (𝑋) → (((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
11396, 112ralrimi 3257 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋)) → ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
114113ex 412 . . . . . . . . 9 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → (𝑓 ∈ 𝒫 (𝑋) → ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
11589, 114ralrimi 3257 . . . . . . . 8 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
11684, 115alrimi 2213 . . . . . . 7 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
1171163exp 1120 . . . . . 6 (𝜑 → (𝑘 ∈ ω → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
118117com12 32 . . . . 5 (𝑘 ∈ ω → (𝜑 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
119118a2d 29 . . . 4 (𝑘 ∈ ω → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
12036, 44, 52, 60, 80, 119finds 7918 . . 3 (if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∈ ω → (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
12128, 120mpcom 38 . 2 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
1222, 3, 4, 5, 6, 23, 121mreexexlemd 17687 1 (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹𝑞 ∧ (𝑞𝐻) ∈ 𝐼))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848  w3a 1087  wal 1538   = wceq 1540  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  cdif 3948  cun 3949  wss 3951  c0 4333  ifcif 4525  𝒫 cpw 4600  {csn 4626   class class class wbr 5143  suc csuc 6386  cfv 6561  ωcom 7887  cen 8982  Fincfn 8985  cardccrd 9975  Moorecmre 17625  mrClscmrc 17626  mrIndcmri 17627
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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-card 9979  df-mre 17629  df-mrc 17630  df-mri 17631
This theorem is referenced by:  mreexdomd  17692  lindsdom  37621  aacllem  49320
  Copyright terms: Public domain W3C validator