P. 67 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6601-6700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ecopovtrng 6601*	Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation ∼, specified by the first hypothesis, is transitive. (Contributed by Jim Kingdon, 1-Sep-2019.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))    ⇒   ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)
Theorem	ecopoverg 6602*	Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation ∼, specified by the first hypothesis, is an equivalence relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))    ⇒   ⊢ ∼ Er (𝑆 × 𝑆)
Theorem	th3qlem1 6603*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ ∼ Er 𝑆    &   ⊢ (((𝑦 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∼ 𝑤 ∧ 𝑧 ∼ 𝑣) → (𝑦 + 𝑧) ∼ (𝑤 + 𝑣)))    ⇒   ⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) → ∃*𝑥∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ))
Theorem	th3qlem2 6604*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ ∈ V    &   ⊢ ∼ Er (𝑆 × 𝑆)    &   ⊢ ((((𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ 𝑓 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((⟨𝑤, 𝑣⟩ ∼ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑠, 𝑓⟩ ∼ ⟨𝑔, ℎ⟩) → (⟨𝑤, 𝑣⟩ + ⟨𝑠, 𝑓⟩) ∼ (⟨𝑢, 𝑡⟩ + ⟨𝑔, ℎ⟩)))    ⇒   ⊢ ((𝐴 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝐵 ∈ ((𝑆 × 𝑆) / ∼ )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [⟨𝑤, 𝑣⟩] ∼ ∧ 𝐵 = [⟨𝑢, 𝑡⟩] ∼ ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ + ⟨𝑢, 𝑡⟩)] ∼ ))
Theorem	th3qcor 6605*	Corollary of Theorem 3Q of [Enderton] p. 60. (Contributed by NM, 12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ ∼ ∈ V    &   ⊢ ∼ Er (𝑆 × 𝑆)    &   ⊢ ((((𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ 𝑓 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((⟨𝑤, 𝑣⟩ ∼ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑠, 𝑓⟩ ∼ ⟨𝑔, ℎ⟩) → (⟨𝑤, 𝑣⟩ + ⟨𝑠, 𝑓⟩) ∼ (⟨𝑢, 𝑡⟩ + ⟨𝑔, ℎ⟩)))    &   ⊢ 𝐺 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ∼ ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ∼ ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ + ⟨𝑢, 𝑡⟩)] ∼ ))}    ⇒   ⊢ Fun 𝐺
Theorem	th3q 6606*	Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ∼ ∈ V    &   ⊢ ∼ Er (𝑆 × 𝑆)    &   ⊢ ((((𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ 𝑓 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((⟨𝑤, 𝑣⟩ ∼ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑠, 𝑓⟩ ∼ ⟨𝑔, ℎ⟩) → (⟨𝑤, 𝑣⟩ + ⟨𝑠, 𝑓⟩) ∼ (⟨𝑢, 𝑡⟩ + ⟨𝑔, ℎ⟩)))    &   ⊢ 𝐺 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ∼ ∧ 𝑦 = [⟨𝑢, 𝑡⟩] ∼ ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ + ⟨𝑢, 𝑡⟩)] ∼ ))}    ⇒   ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([⟨𝐴, 𝐵⟩] ∼ 𝐺[⟨𝐶, 𝐷⟩] ∼ ) = [(⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩)] ∼ )
Theorem	oviec 6607*	Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. See iset.mm for additional comments describing the hypotheses. (Unnecessary distinct variable restrictions were removed by David Abernethy, 4-Jun-2013.) (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 4-Jun-2013.)
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 𝐻 ∈ (𝑆 × 𝑆))    &   ⊢ (((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → 𝐾 ∈ (𝑆 × 𝑆))    &   ⊢ (((𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆)) → 𝐿 ∈ (𝑆 × 𝑆))    &   ⊢ ∼ ∈ V    &   ⊢ ∼ Er (𝑆 × 𝑆)    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ 𝜑))}    &   ⊢ (((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) ∧ (𝑣 = 𝑐 ∧ 𝑢 = 𝑑)) → (𝜑 ↔ 𝜓))    &   ⊢ (((𝑧 = 𝑔 ∧ 𝑤 = ℎ) ∧ (𝑣 = 𝑡 ∧ 𝑢 = 𝑠)) → (𝜑 ↔ 𝜒))    &   ⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝐽))}    &   ⊢ (((𝑤 = 𝑎 ∧ 𝑣 = 𝑏) ∧ (𝑢 = 𝑔 ∧ 𝑓 = ℎ)) → 𝐽 = 𝐾)    &   ⊢ (((𝑤 = 𝑐 ∧ 𝑣 = 𝑑) ∧ (𝑢 = 𝑡 ∧ 𝑓 = 𝑠)) → 𝐽 = 𝐿)    &   ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝐽 = 𝐻)    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [⟨𝑎, 𝑏⟩] ∼ ∧ 𝑦 = [⟨𝑐, 𝑑⟩] ∼ ) ∧ 𝑧 = [(⟨𝑎, 𝑏⟩ + ⟨𝑐, 𝑑⟩)] ∼ ))}    &   ⊢ 𝑄 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ ((((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆))) → ((𝜓 ∧ 𝜒) → 𝐾 ∼ 𝐿))    ⇒   ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([⟨𝐴, 𝐵⟩] ∼ ⨣ [⟨𝐶, 𝐷⟩] ∼ ) = [𝐻] ∼ )
Theorem	ecovcom 6608*	Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6609 instead. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐷, 𝐺⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑥, 𝑦⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )    &   ⊢ 𝐷 = 𝐻    &   ⊢ 𝐺 = 𝐽    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	ecovicom 6609*	Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐷, 𝐺⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑥, 𝑦⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐷 = 𝐻)    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐺 = 𝐽)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	ecovass 6610*	Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6611 will be more useful. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐺, 𝐻⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑁, 𝑄⟩] ∼ )    &   ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝐺, 𝐻⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝐽, 𝐾⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑁, 𝑄⟩] ∼ ) = [⟨𝐿, 𝑀⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆))    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆))    &   ⊢ 𝐽 = 𝐿    &   ⊢ 𝐾 = 𝑀    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	ecoviass 6611*	Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐺, 𝐻⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑁, 𝑄⟩] ∼ )    &   ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝐺, 𝐻⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝐽, 𝐾⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑁, 𝑄⟩] ∼ ) = [⟨𝐿, 𝑀⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆))    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐽 = 𝐿)    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐾 = 𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	ecovdi 6612*	Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6613 will be more helpful. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ )    &   ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆))    &   ⊢ 𝐻 = 𝐾    &   ⊢ 𝐽 = 𝐿    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	ecovidi 6613*	Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ )    &   ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐻 = 𝐾)    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐽 = 𝐿)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
2.6.26  The mapping operation
Syntax	cmap 6614	Extend the definition of a class to include the mapping operation. (Read for 𝐴 ↑𝑚 𝐵, "the set of all functions that map from 𝐵 to 𝐴.)
class ↑𝑚
Syntax	cpm 6615	Extend the definition of a class to include the partial mapping operation. (Read for 𝐴 ↑pm 𝐵, "the set of all partial functions that map from 𝐵 to 𝐴.)
class ↑pm
Definition	df-map 6616*	Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑𝑚 𝐵) (see mapval 6626). Many authors write 𝐴 followed by 𝐵 as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring] p. 95). Other authors show 𝐵 as a prefixed superscript, which is read "𝐴 pre 𝐵 " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(𝐵, 𝐴) for our (𝐴 ↑𝑚 𝐵). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.)
⊢ ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥})
Definition	df-pm 6617*	Define the partial mapping operation. A partial function from 𝐵 to 𝐴 is a function from a subset of 𝐵 to 𝐴. The set of all partial functions from 𝐵 to 𝐴 is written (𝐴 ↑pm 𝐵) (see pmvalg 6625). A notation for this operation apparently does not appear in the literature. We use ↑pm to distinguish it from the less general set exponentiation operation ↑𝑚 (df-map 6616) . See mapsspm 6648 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓})
Theorem	mapprc 6618*	When 𝐴 is a proper class, the class of all functions mapping 𝐴 to 𝐵 is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by NM, 8-Dec-2003.)
⊢ (¬ 𝐴 ∈ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = ∅)
Theorem	pmex 6619*	The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ (Fun 𝑓 ∧ 𝑓 ⊆ (𝐴 × 𝐵))} ∈ V)
Theorem	mapex 6620*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V)
Theorem	fnmap 6621	Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ ↑𝑚 Fn (V × V)
Theorem	fnpm 6622	Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ ↑pm Fn (V × V)
Theorem	reldmmap 6623	Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ Rel dom ↑𝑚
Theorem	mapvalg 6624*	The value of set exponentiation. (𝐴 ↑𝑚 𝐵) is the set of all functions that map from 𝐵 to 𝐴. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑𝑚 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴})
Theorem	pmvalg 6625*	The value of the partial mapping operation. (𝐴 ↑pm 𝐵) is the set of all partial functions that map from 𝐵 to 𝐴. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓})
Theorem	mapval 6626*	The value of set exponentiation (inference version). (𝐴 ↑𝑚 𝐵) is the set of all functions that map from 𝐵 to 𝐴. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑𝑚 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴}
Theorem	elmapg 6627	Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))
Theorem	elmapd 6628	Deduction form of elmapg 6627. (Contributed by BJ, 11-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))
Theorem	mapdm0 6629	The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux, 3-Dec-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ↑𝑚 ∅) = {∅})
Theorem	elpmg 6630	The predicate "is a partial function". (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐶 ∧ 𝐶 ⊆ (𝐵 × 𝐴))))
Theorem	elpm2g 6631	The predicate "is a partial function". (Contributed by NM, 31-Dec-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)))
Theorem	elpm2r 6632	Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵))
Theorem	elpmi 6633	A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.)
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))
Theorem	pmfun 6634	A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → Fun 𝐹)
Theorem	elmapex 6635	Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
Theorem	elmapi 6636	A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴:𝐶⟶𝐵)
Theorem	elmapfn 6637	A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴 Fn 𝐶)
Theorem	elmapfun 6638	A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → Fun 𝐴)
Theorem	elmapssres 6639	A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ ((𝐴 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑𝑚 𝐷))
Theorem	fpmg 6640	A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴))
Theorem	pmss12g 6641	Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷))
Theorem	pmresg 6642	Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵))
Theorem	elmap 6643	Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴)
Theorem	mapval2 6644*	Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑𝑚 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵})
Theorem	elpm 6645	The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (𝐵 × 𝐴)))
Theorem	elpm2 6646	The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))
Theorem	fpm 6647	A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ∈ (𝐵 ↑pm 𝐴))
Theorem	mapsspm 6648	Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ (𝐴 ↑𝑚 𝐵) ⊆ (𝐴 ↑pm 𝐵)
Theorem	pmsspw 6649	Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ↑pm 𝐵) ⊆ 𝒫 (𝐵 × 𝐴)
Theorem	mapsspw 6650	Set exponentiation is a subset of the power set of the Cartesian product of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ↑𝑚 𝐵) ⊆ 𝒫 (𝐵 × 𝐴)
Theorem	fvmptmap 6651*	Special case of fvmpt 5563 for operator theorems. (Contributed by NM, 27-Nov-2007.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝑅 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑𝑚 𝐷) ↦ 𝐵)    ⇒   ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶)
Theorem	map0e 6652	Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 ∅) = 1o)
Theorem	map0b 6653	Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≠ ∅ → (∅ ↑𝑚 𝐴) = ∅)
Theorem	map0g 6654	Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ↑𝑚 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅)))
Theorem	map0 6655	Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ↑𝑚 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅))
Theorem	mapsn 6656*	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
Theorem	mapss 6657	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))
Theorem	fdiagfn 6658*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼))
Theorem	fvdiagfn 6659*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋}))
Theorem	mapsnconst 6660	Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐵 ↑𝑚 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)}))
Theorem	mapsncnv 6661*	Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))
Theorem	mapsnf1o2 6662*	Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ 𝐹:(𝐵 ↑𝑚 𝑆)–1-1-onto→𝐵
Theorem	mapsnf1o3 6663*	Explicit bijection in the reverse of mapsnf1o2 6662. (Contributed by Stefan O'Rear, 24-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))    ⇒   ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑𝑚 𝑆)
2.6.27  Infinite Cartesian products
Syntax	cixp 6664	Extend class notation to include infinite Cartesian products.
class X𝑥 ∈ 𝐴 𝐵
Definition	df-ixp 6665*	Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with 𝑥 ∈ 𝐴 written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually 𝐵 represents a class expression containing 𝑥 free and thus can be thought of as 𝐵(𝑥). Normally, 𝑥 is not free in 𝐴, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.)
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
Theorem	dfixp 6666*	Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 6665, under the assumption that 𝐴 and 𝑥 are disjoint. This way, we can say that 𝑥 is bound in X𝑥 ∈ 𝐴𝐵 even if it appears free in 𝐴. (Contributed by Mario Carneiro, 12-Aug-2016.)
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
Theorem	ixpsnval 6667*	The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.)
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)})
Theorem	elixp2 6668*	Membership in an infinite Cartesian product. See df-ixp 6665 for discussion of the notation. (Contributed by NM, 28-Sep-2006.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	fvixp 6669*	Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷)
Theorem	ixpfn 6670*	A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴)
Theorem	elixp 6671*	Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	elixpconst 6672*	Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	ixpconstg 6673*	Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴))
Theorem	ixpconst 6674*	Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴)
Theorem	ixpeq1 6675*	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ixpeq1d 6676*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ss2ixp 6677	Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2 6678	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dva 6679*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dv 6680*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	cbvixp 6681*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	cbvixpv 6682*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	nfixpxy 6683*	Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon, 15-Feb-2023.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp1 6684	The index variable in an indexed Cartesian product is not free. (Contributed by Jeff Madsen, 19-Jun-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥X𝑥 ∈ 𝐴 𝐵
Theorem	ixpprc 6685*	A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain 𝐴, which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015.)
⊢ (¬ 𝐴 ∈ V → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpf 6686*	A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹:𝐴⟶∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	uniixp 6687*	The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ∪ X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ixpexgg 6688*	The existence of an infinite Cartesian product. 𝑥 is normally a free-variable parameter in 𝐵. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon, 15-Feb-2023.)
⊢ ((𝐴 ∈ 𝑊 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → X𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	ixpin 6689*	The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpiinm 6690*	The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
⊢ (∃𝑧 𝑧 ∈ 𝐵 → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpintm 6691*	The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
⊢ (∃𝑧 𝑧 ∈ 𝐵 → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦)
Theorem	ixp0x 6692	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
⊢ X𝑥 ∈ ∅ 𝐴 = {∅}
Theorem	ixpssmap2g 6693*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 6694 avoids ax-coll 4097. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴))
Theorem	ixpssmapg 6694*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴))
Theorem	0elixp 6695	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴
Theorem	ixpm 6696*	If an infinite Cartesian product of a family 𝐵(𝑥) is inhabited, every 𝐵(𝑥) is inhabited. (Contributed by Mario Carneiro, 22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
⊢ (∃𝑓 𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 → ∀𝑥 ∈ 𝐴 ∃𝑧 𝑧 ∈ 𝐵)
Theorem	ixp0 6697	The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim Kingdon, 16-Feb-2023.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpssmap 6698*	An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)
Theorem	resixp 6699*	Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro, 31-May-2014.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐶) → (𝐹 ↾ 𝐵) ∈ X𝑥 ∈ 𝐵 𝐶)
Theorem	mptelixpg 6700*	Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))