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

Theorem mreexexd 16661
 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 16659 for the base case and mreexexlem4d 16660 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 4994 and ax-ac2 9600. (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 6468 . 2 (𝜑𝑋 ∈ V)
3 mreexexlem2d.5 . 2 (𝜑𝐹 ⊆ (𝑋𝐻))
4 mreexexlem2d.6 . 2 (𝜑𝐺 ⊆ (𝑋𝐻))
5 mreexexlem2d.7 . 2 (𝜑𝐹 ⊆ (𝑁‘(𝐺𝐻)))
6 mreexexlem2d.8 . 2 (𝜑 → (𝐹𝐻) ∈ 𝐼)
7 exmid 923 . . 3 (𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin)
8 ficardid 9101 . . . . . . 7 (𝐹 ∈ Fin → (card‘𝐹) ≈ 𝐹)
98ensymd 8273 . . . . . 6 (𝐹 ∈ Fin → 𝐹 ≈ (card‘𝐹))
10 iftrue 4312 . . . . . 6 (𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐹))
119, 10breqtrrd 4901 . . . . 5 (𝐹 ∈ Fin → 𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
1211a1i 11 . . . 4 (𝜑 → (𝐹 ∈ Fin → 𝐹 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
13 mreexexd.9 . . . . . . . 8 (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))
1413orcanai 1030 . . . . . . 7 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ∈ Fin)
15 ficardid 9101 . . . . . . . 8 (𝐺 ∈ Fin → (card‘𝐺) ≈ 𝐺)
1615ensymd 8273 . . . . . . 7 (𝐺 ∈ Fin → 𝐺 ≈ (card‘𝐺))
1714, 16syl 17 . . . . . 6 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ (card‘𝐺))
18 iffalse 4315 . . . . . . 7 𝐹 ∈ Fin → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
1918adantl 475 . . . . . 6 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) = (card‘𝐺))
2017, 19breqtrrd 4901 . . . . 5 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))
2120ex 403 . . . 4 (𝜑 → (¬ 𝐹 ∈ Fin → 𝐺 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
2212, 21orim12d 992 . . 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 9100 . . . . 5 (𝐹 ∈ Fin → (card‘𝐹) ∈ ω)
2524adantl 475 . . . 4 ((𝜑𝐹 ∈ Fin) → (card‘𝐹) ∈ ω)
26 ficardom 9100 . . . . 5 (𝐺 ∈ Fin → (card‘𝐺) ∈ ω)
2714, 26syl 17 . . . 4 ((𝜑 ∧ ¬ 𝐹 ∈ Fin) → (card‘𝐺) ∈ ω)
2825, 27ifclda 4340 . . 3 (𝜑 → if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∈ ω)
29 breq2 4877 . . . . . . . . . 10 (𝑙 = ∅ → (𝑓𝑙𝑓 ≈ ∅))
30 breq2 4877 . . . . . . . . . 10 (𝑙 = ∅ → (𝑔𝑙𝑔 ≈ ∅))
3129, 30orbi12d 947 . . . . . . . . 9 (𝑙 = ∅ → ((𝑓𝑙𝑔𝑙) ↔ (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅)))
32313anbi1d 1568 . . . . . . . 8 (𝑙 = ∅ → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
3332imbi1d 333 . . . . . . 7 (𝑙 = ∅ → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
34332ralbidv 3198 . . . . . 6 (𝑙 = ∅ → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
3534albidv 2019 . . . . 5 (𝑙 = ∅ → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
3635imbi2d 332 . . . 4 (𝑙 = ∅ → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
37 breq2 4877 . . . . . . . . . 10 (𝑙 = 𝑘 → (𝑓𝑙𝑓𝑘))
38 breq2 4877 . . . . . . . . . 10 (𝑙 = 𝑘 → (𝑔𝑙𝑔𝑘))
3937, 38orbi12d 947 . . . . . . . . 9 (𝑙 = 𝑘 → ((𝑓𝑙𝑔𝑙) ↔ (𝑓𝑘𝑔𝑘)))
40393anbi1d 1568 . . . . . . . 8 (𝑙 = 𝑘 → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
4140imbi1d 333 . . . . . . 7 (𝑙 = 𝑘 → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
42412ralbidv 3198 . . . . . 6 (𝑙 = 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
4342albidv 2019 . . . . 5 (𝑙 = 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
4443imbi2d 332 . . . 4 (𝑙 = 𝑘 → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
45 breq2 4877 . . . . . . . . . 10 (𝑙 = suc 𝑘 → (𝑓𝑙𝑓 ≈ suc 𝑘))
46 breq2 4877 . . . . . . . . . 10 (𝑙 = suc 𝑘 → (𝑔𝑙𝑔 ≈ suc 𝑘))
4745, 46orbi12d 947 . . . . . . . . 9 (𝑙 = suc 𝑘 → ((𝑓𝑙𝑔𝑙) ↔ (𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘)))
48473anbi1d 1568 . . . . . . . 8 (𝑙 = suc 𝑘 → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
4948imbi1d 333 . . . . . . 7 (𝑙 = suc 𝑘 → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
50492ralbidv 3198 . . . . . 6 (𝑙 = suc 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
5150albidv 2019 . . . . 5 (𝑙 = suc 𝑘 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
5251imbi2d 332 . . . 4 (𝑙 = suc 𝑘 → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
53 breq2 4877 . . . . . . . . . 10 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑓𝑙𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
54 breq2 4877 . . . . . . . . . 10 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (𝑔𝑙𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))))
5553, 54orbi12d 947 . . . . . . . . 9 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝑓𝑙𝑔𝑙) ↔ (𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)))))
56553anbi1d 1568 . . . . . . . 8 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
5756imbi1d 333 . . . . . . 7 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ (((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
58572ralbidv 3198 . . . . . 6 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
5958albidv 2019 . . . . 5 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
6059imbi2d 332 . . . 4 (𝑙 = if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑙𝑔𝑙) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ↔ (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺)) ∨ 𝑔 ≈ if(𝐹 ∈ Fin, (card‘𝐹), (card‘𝐺))) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
611ad2antrr 717 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
62 mreexexlem2d.2 . . . . . . . 8 𝑁 = (mrCls‘𝐴)
63 mreexexlem2d.3 . . . . . . . 8 𝐼 = (mrInd‘𝐴)
64 mreexexlem2d.4 . . . . . . . . 9 (𝜑 → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
6564ad2antrr 717 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
66 simplrl 795 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋))
6766elpwid 4390 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ⊆ (𝑋))
68 simplrr 796 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋))
6968elpwid 4390 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑔 ⊆ (𝑋))
70 simpr2 1254 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔)))
71 simpr3 1256 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓) ∈ 𝐼)
72 simpr1 1252 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅))
73 en0 8285 . . . . . . . . . 10 (𝑓 ≈ ∅ ↔ 𝑓 = ∅)
74 en0 8285 . . . . . . . . . 10 (𝑔 ≈ ∅ ↔ 𝑔 = ∅)
7573, 74orbi12i 943 . . . . . . . . 9 ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ↔ (𝑓 = ∅ ∨ 𝑔 = ∅))
7672, 75sylib 210 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓 = ∅ ∨ 𝑔 = ∅))
7761, 62, 63, 65, 67, 69, 70, 71, 76mreexexlem3d 16659 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
7877ex 403 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) → (((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
7978ralrimivva 3180 . . . . 5 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
8079alrimiv 2026 . . . 4 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
81 nfv 2013 . . . . . . . . 9 𝜑
82 nfv 2013 . . . . . . . . 9 𝑘 ∈ ω
83 nfa1 2202 . . . . . . . . 9 𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
8481, 82, 83nf3an 2004 . . . . . . . 8 (𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
85 nfv 2013 . . . . . . . . . 10 𝑓𝜑
86 nfv 2013 . . . . . . . . . 10 𝑓 𝑘 ∈ ω
87 nfra1 3150 . . . . . . . . . . 11 𝑓𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
8887nfal 2355 . . . . . . . . . 10 𝑓𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
8985, 86, 88nf3an 2004 . . . . . . . . 9 𝑓(𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
90 nfv 2013 . . . . . . . . . . . . 13 𝑔𝜑
91 nfv 2013 . . . . . . . . . . . . 13 𝑔 𝑘 ∈ ω
92 nfra2 3155 . . . . . . . . . . . . . 14 𝑔𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
9392nfal 2355 . . . . . . . . . . . . 13 𝑔𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
9490, 91, 93nf3an 2004 . . . . . . . . . . . 12 𝑔(𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
95 nfv 2013 . . . . . . . . . . . 12 𝑔 𝑓 ∈ 𝒫 (𝑋)
9694, 95nfan 2002 . . . . . . . . . . 11 𝑔((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋))
9713ad2ant1 1167 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → 𝐴 ∈ (Moore‘𝑋))
9897ad2antrr 717 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝐴 ∈ (Moore‘𝑋))
99643ad2ant1 1167 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
10099ad2antrr 717 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∀𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
101 simplrl 795 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ∈ 𝒫 (𝑋))
102101elpwid 4390 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ⊆ (𝑋))
103 simplrr 796 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑔 ∈ 𝒫 (𝑋))
104103elpwid 4390 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑔 ⊆ (𝑋))
105 simpr2 1254 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑓 ⊆ (𝑁‘(𝑔)))
106 simpr3 1256 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓) ∈ 𝐼)
107 simpll2 1275 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → 𝑘 ∈ ω)
108 simpll3 1277 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
109 simpr1 1252 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → (𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘))
11098, 62, 63, 100, 102, 104, 105, 106, 107, 108, 109mreexexlem4d 16660 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) ∧ ((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))
111110ex 403 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋) ∧ 𝑔 ∈ 𝒫 (𝑋))) → (((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
112111expr 450 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋)) → (𝑔 ∈ 𝒫 (𝑋) → (((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
11396, 112ralrimi 3166 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋)) → ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
114113ex 403 . . . . . . . . 9 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → (𝑓 ∈ 𝒫 (𝑋) → ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))))
11589, 114ralrimi 3166 . . . . . . . 8 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
11684, 115alrimi 2256 . . . . . . 7 ((𝜑𝑘 ∈ ω ∧ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))
1171163exp 1152 . . . . . 6 (𝜑 → (𝑘 ∈ ω → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
118117com12 32 . . . . 5 (𝑘 ∈ ω → (𝜑 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)) → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
119118a2d 29 . . . 4 (𝑘 ∈ ω → ((𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝑘𝑔𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼))) → (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓 ≈ suc 𝑘𝑔 ≈ suc 𝑘) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑔(𝑓𝑖 ∧ (𝑖) ∈ 𝐼)))))
12036, 44, 52, 60, 80, 119finds 7353 . . 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 16657 1 (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹𝑞 ∧ (𝑞𝐻) ∈ 𝐼))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   ∨ wo 878   ∧ w3a 1111  ∀wal 1654   = wceq 1656   ∈ wcel 2164  ∀wral 3117  ∃wrex 3118  Vcvv 3414   ∖ cdif 3795   ∪ cun 3796   ⊆ wss 3798  ∅c0 4144  ifcif 4306  𝒫 cpw 4378  {csn 4397   class class class wbr 4873  suc csuc 5965  ‘cfv 6123  ωcom 7326   ≈ cen 8219  Fincfn 8222  cardccrd 9074  Moorecmre 16595  mrClscmrc 16596  mrIndcmri 16597 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-om 7327  df-1o 7826  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-card 9078  df-mre 16599  df-mrc 16600  df-mri 16601 This theorem is referenced by:  mreexdomd  16662  lindsdom  33940  aacllem  43436
 Copyright terms: Public domain W3C validator