MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mreexexd Structured version   Visualization version   GIF version
Theorem mreexexd 17596
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 17594 for the base case and mreexexlem4d 17595 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5285 and ax-ac2 10460. (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 6930 . 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 9959 . . . . . . 7 (𝐹 ∈ Fin β†’ (cardβ€˜πΉ) β‰ˆ 𝐹)
98ensymd 9003 . . . . . 6 (𝐹 ∈ Fin β†’ 𝐹 β‰ˆ (cardβ€˜πΉ))
10 iftrue 4534 . . . . . 6 (𝐹 ∈ Fin β†’ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) = (cardβ€˜πΉ))
119, 10breqtrrd 5176 . . . . 5 (𝐹 ∈ Fin β†’ 𝐹 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)))
1211a1i 11 . . . 4 (πœ‘ β†’ (𝐹 ∈ Fin β†’ 𝐹 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ))))
13 mreexexd.9 . . . . . . . 8 (πœ‘ β†’ (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))
1413orcanai 1001 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐹 ∈ Fin) β†’ 𝐺 ∈ Fin)
15 ficardid 9959 . . . . . . . 8 (𝐺 ∈ Fin β†’ (cardβ€˜πΊ) β‰ˆ 𝐺)
1615ensymd 9003 . . . . . . 7 (𝐺 ∈ Fin β†’ 𝐺 β‰ˆ (cardβ€˜πΊ))
1714, 16syl 17 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐹 ∈ Fin) β†’ 𝐺 β‰ˆ (cardβ€˜πΊ))
18 iffalse 4537 . . . . . . 7 (Β¬ 𝐹 ∈ Fin β†’ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) = (cardβ€˜πΊ))
1918adantl 482 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐹 ∈ Fin) β†’ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) = (cardβ€˜πΊ))
2017, 19breqtrrd 5176 . . . . 5 ((πœ‘ ∧ Β¬ 𝐹 ∈ Fin) β†’ 𝐺 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)))
2120ex 413 . . . 4 (πœ‘ β†’ (Β¬ 𝐹 ∈ Fin β†’ 𝐺 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ))))
2212, 21orim12d 963 . . 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 9958 . . . . 5 (𝐹 ∈ Fin β†’ (cardβ€˜πΉ) ∈ Ο‰)
2524adantl 482 . . . 4 ((πœ‘ ∧ 𝐹 ∈ Fin) β†’ (cardβ€˜πΉ) ∈ Ο‰)
26 ficardom 9958 . . . . 5 (𝐺 ∈ Fin β†’ (cardβ€˜πΊ) ∈ Ο‰)
2714, 26syl 17 . . . 4 ((πœ‘ ∧ Β¬ 𝐹 ∈ Fin) β†’ (cardβ€˜πΊ) ∈ Ο‰)
2825, 27ifclda 4563 . . 3 (πœ‘ β†’ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) ∈ Ο‰)
29 breq2 5152 . . . . . . . . . 10 (𝑙 = βˆ… β†’ (𝑓 β‰ˆ 𝑙 ↔ 𝑓 β‰ˆ βˆ…))
30 breq2 5152 . . . . . . . . . 10 (𝑙 = βˆ… β†’ (𝑔 β‰ˆ 𝑙 ↔ 𝑔 β‰ˆ βˆ…))
3129, 30orbi12d 917 . . . . . . . . 9 (𝑙 = βˆ… β†’ ((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ↔ (𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…)))
32313anbi1d 1440 . . . . . . . 8 (𝑙 = βˆ… β†’ (((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) ↔ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)))
3332imbi1d 341 . . . . . . 7 (𝑙 = βˆ… β†’ ((((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ (((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
34332ralbidv 3218 . . . . . 6 (𝑙 = βˆ… β†’ (βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
3534albidv 1923 . . . . 5 (𝑙 = βˆ… β†’ (βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
3635imbi2d 340 . . . 4 (𝑙 = βˆ… β†’ ((πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ↔ (πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))))
37 breq2 5152 . . . . . . . . . 10 (𝑙 = π‘˜ β†’ (𝑓 β‰ˆ 𝑙 ↔ 𝑓 β‰ˆ π‘˜))
38 breq2 5152 . . . . . . . . . 10 (𝑙 = π‘˜ β†’ (𝑔 β‰ˆ 𝑙 ↔ 𝑔 β‰ˆ π‘˜))
3937, 38orbi12d 917 . . . . . . . . 9 (𝑙 = π‘˜ β†’ ((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ↔ (𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜)))
40393anbi1d 1440 . . . . . . . 8 (𝑙 = π‘˜ β†’ (((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) ↔ ((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)))
4140imbi1d 341 . . . . . . 7 (𝑙 = π‘˜ β†’ ((((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ (((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
42412ralbidv 3218 . . . . . 6 (𝑙 = π‘˜ β†’ (βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
4342albidv 1923 . . . . 5 (𝑙 = π‘˜ β†’ (βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
4443imbi2d 340 . . . 4 (𝑙 = π‘˜ β†’ ((πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ↔ (πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))))
45 breq2 5152 . . . . . . . . . 10 (𝑙 = suc π‘˜ β†’ (𝑓 β‰ˆ 𝑙 ↔ 𝑓 β‰ˆ suc π‘˜))
46 breq2 5152 . . . . . . . . . 10 (𝑙 = suc π‘˜ β†’ (𝑔 β‰ˆ 𝑙 ↔ 𝑔 β‰ˆ suc π‘˜))
4745, 46orbi12d 917 . . . . . . . . 9 (𝑙 = suc π‘˜ β†’ ((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ↔ (𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜)))
48473anbi1d 1440 . . . . . . . 8 (𝑙 = suc π‘˜ β†’ (((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) ↔ ((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)))
4948imbi1d 341 . . . . . . 7 (𝑙 = suc π‘˜ β†’ ((((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ (((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
50492ralbidv 3218 . . . . . 6 (𝑙 = suc π‘˜ β†’ (βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
5150albidv 1923 . . . . 5 (𝑙 = suc π‘˜ β†’ (βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
5251imbi2d 340 . . . 4 (𝑙 = suc π‘˜ β†’ ((πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ↔ (πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))))
53 breq2 5152 . . . . . . . . . 10 (𝑙 = if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) β†’ (𝑓 β‰ˆ 𝑙 ↔ 𝑓 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ))))
54 breq2 5152 . . . . . . . . . 10 (𝑙 = if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) β†’ (𝑔 β‰ˆ 𝑙 ↔ 𝑔 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ))))
5553, 54orbi12d 917 . . . . . . . . 9 (𝑙 = if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) β†’ ((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ↔ (𝑓 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) ∨ 𝑔 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)))))
56553anbi1d 1440 . . . . . . . 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 3218 . . . . . 6 (𝑙 = if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) β†’ (βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ 𝑙 ∨ 𝑔 β‰ˆ 𝑙) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) ↔ βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ)) ∨ 𝑔 β‰ˆ if(𝐹 ∈ Fin, (cardβ€˜πΉ), (cardβ€˜πΊ))) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
5958albidv 1923 . . . . 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 724 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
62 mreexexlem2d.2 . . . . . . . 8 𝑁 = (mrClsβ€˜π΄)
63 mreexexlem2d.3 . . . . . . . 8 𝐼 = (mrIndβ€˜π΄)
64 mreexexlem2d.4 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘  ∈ 𝒫 π‘‹βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ ((π‘β€˜(𝑠 βˆͺ {𝑦})) βˆ– (π‘β€˜π‘ ))𝑦 ∈ (π‘β€˜(𝑠 βˆͺ {𝑧})))
6564ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ βˆ€π‘  ∈ 𝒫 π‘‹βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ ((π‘β€˜(𝑠 βˆͺ {𝑦})) βˆ– (π‘β€˜π‘ ))𝑦 ∈ (π‘β€˜(𝑠 βˆͺ {𝑧})))
66 simplrl 775 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž))
6766elpwid 4611 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑓 βŠ† (𝑋 βˆ– β„Ž))
68 simplrr 776 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))
6968elpwid 4611 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑔 βŠ† (𝑋 βˆ– β„Ž))
70 simpr2 1195 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)))
71 simpr3 1196 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ (𝑓 βˆͺ β„Ž) ∈ 𝐼)
72 simpr1 1194 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ (𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…))
73 en0 9015 . . . . . . . . . 10 (𝑓 β‰ˆ βˆ… ↔ 𝑓 = βˆ…)
74 en0 9015 . . . . . . . . . 10 (𝑔 β‰ˆ βˆ… ↔ 𝑔 = βˆ…)
7573, 74orbi12i 913 . . . . . . . . 9 ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ↔ (𝑓 = βˆ… ∨ 𝑔 = βˆ…))
7672, 75sylib 217 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ (𝑓 = βˆ… ∨ 𝑔 = βˆ…))
7761, 62, 63, 65, 67, 69, 70, 71, 76mreexexlem3d 17594 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))
7877ex 413 . . . . . 6 ((πœ‘ ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) β†’ (((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
7978ralrimivva 3200 . . . . 5 (πœ‘ β†’ βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
8079alrimiv 1930 . . . 4 (πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ βˆ… ∨ 𝑔 β‰ˆ βˆ…) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
81 nfv 1917 . . . . . . . . 9 β„²β„Žπœ‘
82 nfv 1917 . . . . . . . . 9 β„²β„Ž π‘˜ ∈ Ο‰
83 nfa1 2148 . . . . . . . . 9 β„²β„Žβˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))
8481, 82, 83nf3an 1904 . . . . . . . 8 β„²β„Ž(πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
85 nfv 1917 . . . . . . . . . 10 β„²π‘“πœ‘
86 nfv 1917 . . . . . . . . . 10 Ⅎ𝑓 π‘˜ ∈ Ο‰
87 nfra1 3281 . . . . . . . . . . 11 β„²π‘“βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))
8887nfal 2316 . . . . . . . . . 10 β„²π‘“βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))
8985, 86, 88nf3an 1904 . . . . . . . . 9 Ⅎ𝑓(πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
90 nfv 1917 . . . . . . . . . . . . 13 β„²π‘”πœ‘
91 nfv 1917 . . . . . . . . . . . . 13 Ⅎ𝑔 π‘˜ ∈ Ο‰
92 nfra2w 3296 . . . . . . . . . . . . . 14 β„²π‘”βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))
9392nfal 2316 . . . . . . . . . . . . 13 β„²π‘”βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))
9490, 91, 93nf3an 1904 . . . . . . . . . . . 12 Ⅎ𝑔(πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
95 nfv 1917 . . . . . . . . . . . 12 Ⅎ𝑔 𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž)
9694, 95nfan 1902 . . . . . . . . . . 11 Ⅎ𝑔((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž))
9713ad2ant1 1133 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
9897ad2antrr 724 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
99643ad2ant1 1133 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) β†’ βˆ€π‘  ∈ 𝒫 π‘‹βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ ((π‘β€˜(𝑠 βˆͺ {𝑦})) βˆ– (π‘β€˜π‘ ))𝑦 ∈ (π‘β€˜(𝑠 βˆͺ {𝑧})))
10099ad2antrr 724 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ βˆ€π‘  ∈ 𝒫 π‘‹βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ ((π‘β€˜(𝑠 βˆͺ {𝑦})) βˆ– (π‘β€˜π‘ ))𝑦 ∈ (π‘β€˜(𝑠 βˆͺ {𝑧})))
101 simplrl 775 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž))
102101elpwid 4611 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑓 βŠ† (𝑋 βˆ– β„Ž))
103 simplrr 776 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))
104103elpwid 4611 . . . . . . . . . . . . . 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 π‘˜))
11098, 62, 63, 100, 102, 104, 105, 106, 107, 108, 109mreexexlem4d 17595 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) ∧ ((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼)) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))
111110ex 413 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) ∧ 𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž))) β†’ (((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
112111expr 457 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž)) β†’ (𝑔 ∈ 𝒫 (𝑋 βˆ– β„Ž) β†’ (((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
11396, 112ralrimi 3254 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) ∧ 𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž)) β†’ βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
114113ex 413 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) β†’ (𝑓 ∈ 𝒫 (𝑋 βˆ– β„Ž) β†’ βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))))
11589, 114ralrimi 3254 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) β†’ βˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
11684, 115alrimi 2206 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ Ο‰ ∧ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))
1171163exp 1119 . . . . . 6 (πœ‘ β†’ (π‘˜ ∈ Ο‰ β†’ (βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))))
118117com12 32 . . . . 5 (π‘˜ ∈ Ο‰ β†’ (πœ‘ β†’ (βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)) β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))))
119118a2d 29 . . . 4 (π‘˜ ∈ Ο‰ β†’ ((πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ π‘˜ ∨ 𝑔 β‰ˆ π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼))) β†’ (πœ‘ β†’ βˆ€β„Žβˆ€π‘“ ∈ 𝒫 (𝑋 βˆ– β„Ž)βˆ€π‘” ∈ 𝒫 (𝑋 βˆ– β„Ž)(((𝑓 β‰ˆ suc π‘˜ ∨ 𝑔 β‰ˆ suc π‘˜) ∧ 𝑓 βŠ† (π‘β€˜(𝑔 βˆͺ β„Ž)) ∧ (𝑓 βˆͺ β„Ž) ∈ 𝐼) β†’ βˆƒπ‘– ∈ 𝒫 𝑔(𝑓 β‰ˆ 𝑖 ∧ (𝑖 βˆͺ β„Ž) ∈ 𝐼)))))
12036, 44, 52, 60, 80, 119finds 7891 . . 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 17592 1 (πœ‘ β†’ βˆƒπ‘ž ∈ 𝒫 𝐺(𝐹 β‰ˆ π‘ž ∧ (π‘ž βˆͺ 𝐻) ∈ 𝐼))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   ∨ wo 845   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βˆ– cdif 3945   βˆͺ cun 3946   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  π’« cpw 4602  {csn 4628   class class class wbr 5148  suc csuc 6366  β€˜cfv 6543  Ο‰com 7857   β‰ˆ cen 8938  Fincfn 8941  cardccrd 9932  Moorecmre 17530  mrClscmrc 17531  mrIndcmri 17532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7858  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936  df-mre 17534  df-mrc 17535  df-mri 17536
This theorem is referenced by:  mreexdomd  17597  lindsdom  36785  aacllem  47936
  Copyright terms: Public domain W3C validator