 Home Metamath Proof ExplorerTheorem List (p. 336 of 429) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-27903) Hilbert Space Explorer (27904-29428) Users' Mathboxes (29429-42879)

Theorem List for Metamath Proof Explorer - 33501-33600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremwl-ax11-lem10 33501* We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 183 can be used in conjunction with wl-ax11-lem9 33500 to eliminate the second antecedent. Missing is something along the lines of ax-6 1945, so we could remove the first antecedent. But the Metamath axioms cannot accomplish this. Such a rule must reside one abstraction level higher than all others: It says that a distinctor implies a distinct variable condition on its contained setvar. This is only needed if such conditions are required, as ax-11v does. The result of this study is for me, that you cannot introduce a setvar capturing this condition, and hope to eliminate it later. (Contributed by Wolf Lammen, 30-Jun-2019.)
(∀𝑦 𝑦 = 𝑢 → (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)))

Theoremwl-sbcom3 33502 Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Copy of ~? sbcom3OLD with a shortened proof.

Keep this theorem for a while here because an external reference to it exists.

(Contributed by Giovanni Mascellani, 8-Apr-2018.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑧 / 𝑦]𝜑)

20.17.5  1. Bootstrapping classes

Syntaxwcel-wl 33503 Redefine in a class context to avoid overloading and syntax check errors in mmj2. This operator requires 𝑥 and 𝐵 distinct.
wff 𝑥𝐵

Theoremwel-wl 33504 Redefine in a set context to avoid syntax check errors in mmj2. 𝑥 and 𝑦 must be distinct. (Contributed by Wolf Lammen, 27-Nov-2021.)
wff 𝑥𝑦

Syntaxwcel2-wl 33505 Redefine in a class context to avoid overloading and syntax check errors in mmj2. 𝑥 and 𝐵 may not be distinct.
wff 𝑥𝐵

Theoremwel2-wl 33506 Redefine in a set context to avoid syntax check errors in mmj2. It is no syntactic error to assign the same variable to 𝑥 and 𝑦. (Contributed by Wolf Lammen, 27-Nov-2021.)
wff 𝑥𝑦

Axiomax-wl-8cl 33507* In ZFC, as presented in this document, classes are meant to be just a notational convenience, that can be reduced to pure set theory by means of df-clab 2638 (there stated in the eliminable property). That is, in an expression 𝑥𝐴, the class variable 𝐴 is implicitely assumed to represent an expression {𝑧𝜑} with some appropriate 𝜑. Unfortunately, 𝜑 syntactically covers any well-formed formula (wff), including 𝑧𝐴. This choice inevitably breaks the stated property. And it potentially carries over to any expression containing class variables. To fix this, a simple rule could exclude class variables at all in a class defining wff. A more elaborate rule could detect, and limit exclusion to proper classes (potentially problematic). In any case, the verification process should enforce any such rule during replacement, which it currently does not. The result is that we rely on the awareness of theorem designers to this problem. It seems, in ZFC proper classes are reduced to a few instances only, so a careful study may reveal that this limited use does not impose logical loop holes. It must be said, still, this necessary extra knowledge contradicts the general philosophy of Metamath, trying to establish certainty by a machine executable confirmation.

An extension to ZFC allows classes to exist on their own. Classes are then extensions to sets, also seamlessly extending the idea of elementhood. In order to move from the general to the specific, sets presuppose classes, so classes should be introduced first. This is somewhat in opposition to the classic order of introduction of syntactic elements, but has been carried out in the past, for example by the von-Neumann theory of classes.

In the context of Metamath, which is a purely text-based syntactical concept, no semantics are imposed at the very beginning on classes. Instead axioms will narrow down bit by bit how elementhood behaves in proofs, of course always with the intuitive understanding of a human in mind.

One basic property of elementhood we expect is that the 'element' is replaceable with something equal to it. Or that equality is finer grained than the elementhood relation. This idea is formally expressed in terms coined 'implicit substitution' in this document: ((𝑥 = 𝑦) → (𝑥𝐴𝑦𝐴)). This axiom prepares this notation.

Note that particular constructions of classes like that in df-clab 2638 in fact allow to prove this axiom. Can we expect to eliminate this axiom then? No, the generalizing term still refers to an unexplained subterm 𝑥𝐴, so this axiom recurs in the general case. On the other hand, our axiom here stays true, even when just the existence of a class is known, as is often the case after applying the axiom of choice, without a chance to actually construct it.

We provide a version of this axiom, that requires all variables to be distinct. Step by step these restrictions are lifted, in the end covering the most general term 𝐴𝐵.

This axiom is meant as a replacement for ax-8 2032. (Contributed by Wolf Lammen, 27-Nov-2021.)

(𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))

Theoremwl-ax8clv1 33508* Lifting the distinct variable constraint on 𝑥 and 𝑦 in ax-wl-8cl 33507. (Contributed by Wolf Lammen, 27-Nov-2021.)
(𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))

Theoremwl-clelv2-just 33509* Show that the definition df-wl-clelv2 33510 is conservative. (Contributed by Wolf Lammen, 27-Nov-2021.)
(𝑥𝐴 ↔ ∀𝑢(𝑢 = 𝑥𝑢𝐴))

Definitiondf-wl-clelv2 33510* Define the term 𝑥𝐴, 𝑥 in 𝐴 permitted. (Contributed by Wolf Lammen, 27-Nov-2021.)
(𝑥𝐴 ↔ ∀𝑢(𝑢 = 𝑥𝑢𝐴))

Theoremwl-ax8clv2 33511 Axiom ax-wl-8cl 33507 carries over to our new definition df-wl-clelv2 33510. (Contributed by Wolf Lammen, 27-Nov-2021.)
(𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))

20.18  Mathbox for Brendan Leahy

Theoremrabiun 33512* Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.)
{𝑥 𝑦𝐴 𝐵𝜑} = 𝑦𝐴 {𝑥𝐵𝜑}

Theoremiundif1 33513* Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.)
𝑥𝐴 (𝐵𝐶) = ( 𝑥𝐴 𝐵𝐶)

Theoremimadifss 33514 The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.)
((𝐹𝐴) ∖ (𝐹𝐵)) ⊆ (𝐹 “ (𝐴𝐵))

Theoremcureq 33515 Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
(𝐴 = 𝐵 → curry 𝐴 = curry 𝐵)

Theoremunceq 33516 Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
(𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵)

Theoremcurf 33517 Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → curry 𝐹:𝐴⟶(𝐶𝑚 𝐵))

Theoremuncf 33518 Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
(𝐹:𝐴⟶(𝐶𝑚 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶)

Theoremcurfv 33519 Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
(((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴𝑉𝐵𝑊) ∧ 𝑊𝑋) → ((curry 𝐹𝐴)‘𝐵) = (𝐴𝐹𝐵))

Theoremuncov 33520 Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
((𝐴𝑉𝐵𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹𝐴)‘𝐵))

Theoremcurunc 33521 Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
((𝐹:𝐴⟶(𝐶𝑚 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹)

Theoremunccur 33522 Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.)
((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → uncurry curry 𝐹 = 𝐹)

Theoremphpreu 33523* Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.)
((𝐴 ∈ Fin ∧ 𝐴𝐵) → (∀𝑥𝐴𝑦𝐵 𝑥 = 𝐶 ↔ ∀𝑥𝐴 ∃!𝑦𝐵 𝑥 = 𝐶))

Theoremfinixpnum 33524* A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.)
((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ dom card) → X𝑥𝐴 𝐵 ∈ dom card)

Theoremfin2solem 33525* Lemma for fin2so 33526. (Contributed by Brendan Leahy, 29-Jun-2019.)
((𝑅 Or 𝑥 ∧ (𝑦𝑥𝑧𝑥)) → (𝑦𝑅𝑧 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑧}))

Theoremfin2so 33526 Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.)
((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ Fin)

Theoremltflcei 33527 Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) < 𝐵𝐴 < -(⌊‘-𝐵)))

Theoremleceifl 33528 Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-(⌊‘-𝐴) ≤ 𝐵𝐴 ≤ (⌊‘𝐵)))

Theoremsin2h 33529 Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.)
(𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2)))

Theoremcos2h 33530 Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.)
(𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2)))

Theoremtan2h 33531 Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.)
(𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))

Theorempigt3 33532 π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
3 < π

Theoremlindsdom 33533 A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021.)
((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋𝐼)

Theoremlindsenlbs 33534 A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021.)
(((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋𝐼) → 𝑋 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))

Theoremmatunitlindflem1 33535 One direction of matunitlindf 33537. (Contributed by Brendan Leahy, 2-Jun-2021.)
(((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g𝑅)))

Theoremmatunitlindflem2 33536 One direction of matunitlindf 33537. (Contributed by Brendan Leahy, 2-Jun-2021.)
((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))

Theoremmatunitlindf 33537 A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.)
((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))

Theoremptrest 33538* Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.)
(𝜑𝐴𝑉)    &   (𝜑𝐹:𝐴⟶Top)    &   ((𝜑𝑘𝐴) → 𝑆𝑊)       (𝜑 → ((∏t𝐹) ↾t X𝑘𝐴 𝑆) = (∏t‘(𝑘𝐴 ↦ ((𝐹𝑘) ↾t 𝑆))))

Theoremptrecube 33539* Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.)
𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))       ((𝑆𝑅𝑃𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈ (1...𝑁)((𝑃𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)

Theorempoimirlem1 33540* Lemma for poimir 33572- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))    &   (𝜑𝑇:(1...𝑁)⟶ℤ)    &   (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   (𝜑𝑀 ∈ (1...(𝑁 − 1)))       (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛))

Theorempoimirlem2 33541* Lemma for poimir 33572- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))    &   (𝜑𝑇:(1...𝑁)⟶ℤ)    &   (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   (𝜑𝑉 ∈ (1...(𝑁 − 1)))    &   (𝜑𝑀 ∈ ((0...𝑁) ∖ {𝑉}))       (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛))

Theorempoimirlem3 33542* Lemma for poimir 33572 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑀 < 𝑁)    &   (𝜑𝑇:(1...𝑀)⟶(0..^𝐾))    &   (𝜑𝑈:(1...𝑀)–1-1-onto→(1...𝑀))       (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵 → (⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))))

Theorempoimirlem4 33543* Lemma for poimir 33572 connecting the admissible faces on the back face of the (𝑀 + 1)-cube to admissible simplices in the 𝑀-cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑀 < 𝑁)       (𝜑 → {𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑀)) × {𝑓𝑓:(1...𝑀)–1-1-onto→(1...𝑀)}) ∣ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝𝐵} ≈ {𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∣ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝𝐵 ∧ ((1st𝑠)‘(𝑀 + 1)) = 0 ∧ ((2nd𝑠)‘(𝑀 + 1)) = (𝑀 + 1))})

Theorempoimirlem5 33544* Lemma for poimir 33572 to establish that, for the simplices defined by a walk along the edges of an 𝑁-cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝑇𝑆)    &   (𝜑 → 0 < (2nd𝑇))       (𝜑 → (𝐹‘0) = (1st ‘(1st𝑇)))

Theorempoimirlem6 33545* Lemma for poimir 33572 establishing, for a face of a simplex defined by a walk along the edges of an 𝑁-cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))    &   (𝜑𝑀 ∈ (1...((2nd𝑇) − 1)))       (𝜑 → (𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛)) = ((2nd ‘(1st𝑇))‘𝑀))

Theorempoimirlem7 33546* Lemma for poimir 33572, similar to poimirlem6 33545, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))    &   (𝜑𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁))       (𝜑 → (𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st𝑇))‘𝑀))

Theorempoimirlem8 33547* Lemma for poimir 33572, establishing that away from the opposite vertex the walks in poimirlem9 33548 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))    &   (𝜑𝑈𝑆)       (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))

Theorempoimirlem9 33548* Lemma for poimir 33572, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))    &   (𝜑𝑈𝑆)    &   (𝜑 → (2nd ‘(1st𝑈)) ≠ (2nd ‘(1st𝑇)))       (𝜑 → (2nd ‘(1st𝑈)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))

Theorempoimirlem10 33549* Lemma for poimir 33572 establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) = 0)       (𝜑 → ((𝐹‘(𝑁 − 1)) ∘𝑓 − ((1...𝑁) × {1})) = (1st ‘(1st𝑇)))

Theorempoimirlem11 33550* Lemma for poimir 33572 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) = 0)    &   (𝜑𝑈𝑆)    &   (𝜑 → (2nd𝑈) = 0)    &   (𝜑𝑀 ∈ (1...𝑁))       (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑀)))

Theorempoimirlem12 33551* Lemma for poimir 33572 connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) = 𝑁)    &   (𝜑𝑈𝑆)    &   (𝜑 → (2nd𝑈) = 𝑁)    &   (𝜑𝑀 ∈ (0...(𝑁 − 1)))       (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑀)))

Theorempoimirlem13 33552* Lemma for poimir 33572- for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))       (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 0)

Theorempoimirlem14 33553* Lemma for poimir 33572- for at most one simplex associated with a shared face is the opposite vertex last on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))       (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)

Theorempoimirlem15 33554* Lemma for poimir 33572, that the face in poimirlem22 33561 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))       (𝜑 → ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ 𝑆)

Theorempoimirlem16 33555* Lemma for poimir 33572 establishing the vertices of the simplex of poimirlem17 33556. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)    &   (𝜑 → (2nd𝑇) = 0)       (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))

Theorempoimirlem17 33556* Lemma for poimir 33572 establishing existence for poimirlem18 33557. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)    &   (𝜑 → (2nd𝑇) = 0)       (𝜑 → ∃𝑧𝑆 𝑧𝑇)

Theorempoimirlem18 33557* Lemma for poimir 33572 stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)    &   (𝜑 → (2nd𝑇) = 0)       (𝜑 → ∃!𝑧𝑆 𝑧𝑇)

Theorempoimirlem19 33558* Lemma for poimir 33572 establishing the vertices of the simplex in poimirlem20 33559. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)    &   (𝜑 → (2nd𝑇) = 𝑁)       (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))))

Theorempoimirlem20 33559* Lemma for poimir 33572 establishing existence for poimirlem21 33560. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)    &   (𝜑 → (2nd𝑇) = 𝑁)       (𝜑 → ∃𝑧𝑆 𝑧𝑇)

Theorempoimirlem21 33560* Lemma for poimir 33572 stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)    &   (𝜑 → (2nd𝑇) = 𝑁)       (𝜑 → ∃!𝑧𝑆 𝑧𝑇)

Theorempoimirlem22 33561* Lemma for poimir 33572, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   (𝜑𝑇𝑆)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)    &   ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)       (𝜑 → ∃!𝑧𝑆 𝑧𝑇)

Theorempoimirlem23 33562* Lemma for poimir 33572, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))    &   (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   (𝜑𝑉 ∈ (0...𝑁))       (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))

Theorempoimirlem24 33563* Lemma for poimir 33572, two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))    &   (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   (𝜑𝑉 ∈ (0...𝑁))       (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0)) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))))

Theorempoimirlem25 33564* Lemma for poimir 33572 stating that for a given simplex such that no vertex maps to 𝑁, the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))    &   (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁𝑇, 𝑈⟩ / 𝑠𝐶)       (𝜑 → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))

Theorempoimirlem26 33565* Lemma for poimir 33572 showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))       (𝜑 → 2 ∥ ((#‘{𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd𝑡)})𝑖 = (1st𝑡) / 𝑠𝐶}) − (#‘{𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶})))

Theorempoimirlem27 33566* Lemma for poimir 33572 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝𝑛) = 0)) → 𝐵 < 𝑛)    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1))       (𝜑 → 2 ∥ ((#‘{𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd𝑡)})𝑖 = (1st𝑡) / 𝑠𝐶}) − (#‘{𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ (0...(𝑁 − 1))𝑖 = 𝐶 ∧ ((1st𝑠)‘𝑁) = 0 ∧ ((2nd𝑠)‘𝑁) = 𝑁)})))

Theorempoimirlem28 33567* Lemma for poimir 33572, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝𝑛) = 0)) → 𝐵 < 𝑛)    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1))    &   (𝜑𝐾 ∈ ℕ)       (𝜑 → ∃𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶)

Theorempoimirlem29 33568* Lemma for poimir 33572 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))    &   𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)    &   (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))    &   ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)       (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))

Theorempoimirlem30 33569* Lemma for poimir 33572 combining poimirlem29 33568 with bwth 21261. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))    &   𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)    &   (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))    &   ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)       (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))

Theorempoimirlem31 33570* Lemma for poimir 33572, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 33569 and poimirlem28 33567. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)    &   𝑃 = ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))    &   (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))    &   ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))       ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))

Theorempoimirlem32 33571* Lemma for poimir 33572, combining poimirlem28 33567, poimirlem30 33569, and poimirlem31 33570 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛))       (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))

Theorempoimir 33572* Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)    &   ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛))       (𝜑 → ∃𝑐𝐼 (𝐹𝑐) = ((1...𝑁) × {0}))

Theorembroucube 33573* Brouwer - or as Kulpa calls it, "Bohl-Brouwer" - fixed point theorem for the unit cube. Theorem on [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
(𝜑𝑁 ∈ ℕ)    &   𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn (𝑅t 𝐼)))       (𝜑 → ∃𝑐𝐼 𝑐 = (𝐹𝑐))

Theoremheicant 33574 Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.) (Proof shortened by AV, 27-Sep-2020.)
(𝜑𝐶 ∈ (∞Met‘𝑋))    &   (𝜑𝐷 ∈ (∞Met‘𝑌))    &   (𝜑 → (MetOpen‘𝐶) ∈ Comp)    &   (𝜑𝑋 ≠ ∅)    &   (𝜑𝑌 ≠ ∅)       (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))

Theoremopnmbllem0 33575* Lemma for ismblfin 33580; could also be used to shorten proof of opnmbllem 23415. (Contributed by Brendan Leahy, 13-Jul-2018.)
(𝐴 ∈ (topGen‘ran (,)) → ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)

Theoremmblfinlem1 33576* Lemma for ismblfin 33580, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in 𝐴. (Contributed by Brendan Leahy, 13-Jul-2018.)
((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})

Theoremmblfinlem2 33577* Lemma for ismblfin 33580, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑀 ∈ ℝ ∧ 𝑀 < (vol*‘𝐴)) → ∃𝑠 ∈ (Clsd‘(topGen‘ran (,)))(𝑠𝐴𝑀 < (vol*‘𝑠)))

Theoremmblfinlem3 33578* The difference between two sets measurable by the criterion in ismblfin 33580 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
(((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) ∧ ((vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < ) ∧ (vol*‘𝐵) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐵𝑦 = (vol‘𝑏))}, ℝ, < ))) → sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ (𝐴𝐵) ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) = (vol*‘(𝐴𝐵)))

Theoremmblfinlem4 33579* Backward direction of ismblfin 33580. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
(((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ 𝐴 ∈ dom vol) → (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < ))

Theoremismblfin 33580* Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.)
((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐴 ∈ dom vol ↔ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏𝐴𝑦 = (vol‘𝑏))}, ℝ, < )))

Theoremovoliunnfl 33581* ovoliun 23319 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.)
((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) ∈ ℝ)) → (vol*‘ 𝑚 ∈ ℕ (𝑓𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))), ℝ*, < ))       ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)

Theoremex-ovoliunnfl 33582* Demonstration of ovoliunnfl 33581. (Contributed by Brendan Leahy, 21-Nov-2017.)
((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)

Theoremvoliunnfl 33583* voliun 23368 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.)
𝑆 = seq1( + , 𝐺)    &   𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))    &   ((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < ))       ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)

Theoremvolsupnfl 33584* volsup 23370 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.)
((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))       ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)

Theorem0mbf 33585 The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.)
∅ ∈ MblFn

Theoremmbfresfi 33586* Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.)
(𝜑𝐹:𝐴⟶ℂ)    &   (𝜑𝑆 ∈ Fin)    &   (𝜑 → ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn)    &   (𝜑 𝑆 = 𝐴)       (𝜑𝐹 ∈ MblFn)

Theoremmbfposadd 33587* If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018.)
(𝜑 → (𝑥𝐴𝐵) ∈ MblFn)    &   ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)    &   (𝜑 → (𝑥𝐴𝐶) ∈ MblFn)    &   ((𝜑𝑥𝐴) → 𝐶 ∈ ℝ)    &   (𝜑 → (𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)       (𝜑 → (𝑥𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)

Theoremcnambfre 33588 A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.)
((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ (((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → 𝐹 ∈ MblFn)

Theoremdvtanlem 33589 Lemma for dvtan 33590- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) (Proof shortened by OpenAI, 3-Jul-2020.)
(cos “ (ℂ ∖ {0})) ∈ (TopOpen‘ℂfld)

Theoremdvtan 33590 Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.)
(ℂ D tan) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2))

Theoremitg2addnclem 33591* An alternate expression for the 2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.)
𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(∃𝑦 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑔𝑧) = 0, 0, ((𝑔𝑧) + 𝑦))) ∘𝑟𝐹𝑥 = (∫1𝑔))}       (𝐹:ℝ⟶(0[,]+∞) → (∫2𝐹) = sup(𝐿, ℝ*, < ))

Theoremitg2addnclem2 33592* Lemma for itg2addnc 33594. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.)
(𝜑𝐹 ∈ MblFn)    &   (𝜑𝐹:ℝ⟶(0[,)+∞))       (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ dom ∫1)

Theoremitg2addnclem3 33593* Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 33594. (Contributed by Brendan Leahy, 11-Mar-2018.)
(𝜑𝐹 ∈ MblFn)    &   (𝜑𝐹:ℝ⟶(0[,)+∞))    &   (𝜑 → (∫2𝐹) ∈ ℝ)    &   (𝜑𝐺:ℝ⟶(0[,)+∞))    &   (𝜑 → (∫2𝐺) ∈ ℝ)       (𝜑 → (∃ ∈ dom ∫1(∃𝑦 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑧) = 0, 0, ((𝑧) + 𝑦))) ∘𝑟 ≤ (𝐹𝑓 + 𝐺) ∧ 𝑠 = (∫1)) → ∃𝑡𝑢(∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1((∃𝑐 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑓𝑧) = 0, 0, ((𝑓𝑧) + 𝑐))) ∘𝑟𝐹𝑡 = (∫1𝑓)) ∧ (∃𝑑 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑔𝑧) = 0, 0, ((𝑔𝑧) + 𝑑))) ∘𝑟𝐺𝑢 = (∫1𝑔))) ∧ 𝑠 = (𝑡 + 𝑢))))

Theoremitg2addnc 33594 Alternate proof of itg2add 23571 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 23520, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 9295, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.)
(𝜑𝐹 ∈ MblFn)    &   (𝜑𝐹:ℝ⟶(0[,)+∞))    &   (𝜑 → (∫2𝐹) ∈ ℝ)    &   (𝜑𝐺:ℝ⟶(0[,)+∞))    &   (𝜑 → (∫2𝐺) ∈ ℝ)       (𝜑 → (∫2‘(𝐹𝑓 + 𝐺)) = ((∫2𝐹) + (∫2𝐺)))

Theoremitg2gt0cn 33595* itg2gt0 23572 holds on functions continuous on an open interval in the absence of ax-cc 9295. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)
(𝜑𝑋 < 𝑌)    &   (𝜑𝐹:ℝ⟶(0[,)+∞))    &   ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹𝑥))    &   (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))       (𝜑 → 0 < (∫2𝐹))

Theoremibladdnclem 33596* Lemma for ibladdnc 33597; cf ibladdlem 23631, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 33594. (Contributed by Brendan Leahy, 31-Oct-2017.)
((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)    &   ((𝜑𝑥𝐴) → 𝐶 ∈ ℝ)    &   ((𝜑𝑥𝐴) → 𝐷 = (𝐵 + 𝐶))    &   (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)    &   (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)    &   (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)       (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)

Theoremibladdnc 33597* Choice-free analogue of itgadd 23636. A measurability hypothesis is necessitated by the loss of mbfadd 23473; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.)
((𝜑𝑥𝐴) → 𝐵𝑉)    &   (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)    &   ((𝜑𝑥𝐴) → 𝐶𝑉)    &   (𝜑 → (𝑥𝐴𝐶) ∈ 𝐿1)    &   (𝜑 → (𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)       (𝜑 → (𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1)