Theorem List for Intuitionistic Logic Explorer - 6601-6700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | erovlem 6601* |
Lemma for eroprf 6602. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) |
|
Theorem | eroprf 6602* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} & ⊢ (𝜑 → 𝑅 ∈ 𝑋)
& ⊢ (𝜑 → 𝑆 ∈ 𝑌)
& ⊢ 𝐿 = (𝐶 / 𝑇) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐾)⟶𝐿) |
|
Theorem | eroprf2 6603* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) |
|
Theorem | ecopoveq 6604* |
This is the first of several theorems about equivalence relations of
the kind used in construction of fractions and signed reals, involving
operations on equivalent classes of ordered pairs. This theorem
expresses the relation ∼ (specified
by the hypothesis) in terms
of its operation 𝐹. (Contributed by NM, 16-Aug-1995.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
|
Theorem | ecopovsym 6605* |
Assuming the operation 𝐹 is commutative, show that the
relation
∼, specified
by the first hypothesis, is symmetric.
(Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) ⇒ ⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴) |
|
Theorem | ecopovtrn 6606* |
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 NM, 11-Feb-1996.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶) |
|
Theorem | ecopover 6607* |
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 NM, 16-Feb-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ∼ Er (𝑆 × 𝑆) |
|
Theorem | ecopovsymg 6608* |
Assuming the operation 𝐹 is commutative, show that the
relation
∼, specified
by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴) |
|
Theorem | ecopovtrng 6609* |
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 6610* |
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 6611* |
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 6612* |
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 6613* |
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 6614* |
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 6615* |
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 6616* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6617 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ 𝐷 = 𝐻
& ⊢ 𝐺 = 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | ecovicom 6617* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐷 = 𝐻)
& ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐺 = 𝐽) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | ecovass 6618* |
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6619 will be more useful. (Contributed by NM,
31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐺, 𝐻〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑁, 𝑄〉] ∼ ) & ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ ) = [〈𝐿, 𝑀〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) & ⊢ 𝐽 = 𝐿
& ⊢ 𝐾 = 𝑀 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
|
Theorem | ecoviass 6619* |
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16-Sep-2019.)
|
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐺, 𝐻〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑁, 𝑄〉] ∼ ) & ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ ) = [〈𝐿, 𝑀〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐽 = 𝐿)
& ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐾 = 𝑀) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
|
Theorem | ecovdi 6620* |
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6621 will be more helpful. (Contributed by NM,
2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑀, 𝑁〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑀, 𝑁〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑧, 𝑤〉] ∼ ) = [〈𝑊, 𝑋〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑣, 𝑢〉] ∼ ) = [〈𝑌, 𝑍〉] ∼ ) & ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([〈𝑊, 𝑋〉] ∼ + [〈𝑌, 𝑍〉] ∼ ) = [〈𝐾, 𝐿〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) & ⊢ 𝐻 = 𝐾
& ⊢ 𝐽 = 𝐿 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
|
Theorem | ecovidi 6621* |
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 6622 |
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 6623 |
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 6624* |
Define the mapping operation or set exponentiation. The set of all
functions that map from 𝐵 to 𝐴 is written (𝐴
↑𝑚 𝐵) (see
mapval 6634). 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 6625* |
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 6633). 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 6624) . See mapsspm 6656 for
its relationship to set exponentiation. (Contributed by NM,
15-Nov-2007.)
|
⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) |
|
Theorem | mapprc 6626* |
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 6627* |
The class of all partial functions from one set to another is a set.
(Contributed by NM, 15-Nov-2007.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ (Fun 𝑓 ∧ 𝑓 ⊆ (𝐴 × 𝐵))} ∈ V) |
|
Theorem | mapex 6628* |
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 6629 |
Set exponentiation has a universal domain. (Contributed by NM,
8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
⊢ ↑𝑚 Fn (V ×
V) |
|
Theorem | fnpm 6630 |
Partial function exponentiation has a universal domain. (Contributed by
Mario Carneiro, 14-Nov-2013.)
|
⊢ ↑pm Fn (V ×
V) |
|
Theorem | reldmmap 6631 |
Set exponentiation is a well-behaved binary operator. (Contributed by
Stefan O'Rear, 27-Feb-2015.)
|
⊢ Rel dom
↑𝑚 |
|
Theorem | mapvalg 6632* |
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 6633* |
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 6634* |
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 6635 |
Membership relation for set exponentiation. (Contributed by NM,
17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
|
Theorem | elmapd 6636 |
Deduction form of elmapg 6635. (Contributed by BJ, 11-Apr-2020.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
|
Theorem | mapdm0 6637 |
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 6638 |
The predicate "is a partial function". (Contributed by Mario
Carneiro,
14-Nov-2013.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐶 ∧ 𝐶 ⊆ (𝐵 × 𝐴)))) |
|
Theorem | elpm2g 6639 |
The predicate "is a partial function". (Contributed by NM,
31-Dec-2013.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))) |
|
Theorem | elpm2r 6640 |
Sufficient condition for being a partial function. (Contributed by NM,
31-Dec-2013.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) |
|
Theorem | elpmi 6641 |
A partial function is a function. (Contributed by Mario Carneiro,
15-Sep-2015.)
|
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) |
|
Theorem | pmfun 6642 |
A partial function is a function. (Contributed by Mario Carneiro,
30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → Fun 𝐹) |
|
Theorem | elmapex 6643 |
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 6644 |
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴:𝐶⟶𝐵) |
|
Theorem | elmapfn 6645 |
A mapping is a function with the appropriate domain. (Contributed by AV,
6-Apr-2019.)
|
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴 Fn 𝐶) |
|
Theorem | elmapfun 6646 |
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 6647 |
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|
⊢ ((𝐴 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑𝑚 𝐷)) |
|
Theorem | fpmg 6648 |
A total function is a partial function. (Contributed by Mario Carneiro,
31-Dec-2013.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴)) |
|
Theorem | pmss12g 6649 |
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31-Dec-2013.)
|
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷)) |
|
Theorem | pmresg 6650 |
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31-Dec-2013.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
|
Theorem | elmap 6651 |
Membership relation for set exponentiation. (Contributed by NM,
8-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴) |
|
Theorem | mapval2 6652* |
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3-Nov-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ↑𝑚 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵}) |
|
Theorem | elpm 6653 |
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 6654 |
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 6655 |
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 6656 |
Set exponentiation is a subset of partial maps. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
|
⊢ (𝐴 ↑𝑚 𝐵) ⊆ (𝐴 ↑pm 𝐵) |
|
Theorem | pmsspw 6657 |
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 6658 |
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 6659* |
Special case of fvmpt 5571 for operator theorems. (Contributed by NM,
27-Nov-2007.)
|
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝑅 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑𝑚 𝐷) ↦ 𝐵) ⇒ ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶) |
|
Theorem | map0e 6660 |
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 6661 |
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 6662 |
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 6663 |
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 6664* |
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 6665 |
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 6666* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
|
Theorem | fvdiagfn 6667* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋})) |
|
Theorem | mapsnconst 6668 |
Every singleton map is a constant function. (Contributed by Stefan
O'Rear, 25-Mar-2015.)
|
⊢ 𝑆 = {𝑋}
& ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈
V ⇒ ⊢ (𝐹 ∈ (𝐵 ↑𝑚 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)})) |
|
Theorem | mapsncnv 6669* |
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 6670* |
Explicit bijection between a set and its singleton functions.
(Contributed by Stefan O'Rear, 21-Mar-2015.)
|
⊢ 𝑆 = {𝑋}
& ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ 𝐹:(𝐵 ↑𝑚 𝑆)–1-1-onto→𝐵 |
|
Theorem | mapsnf1o3 6671* |
Explicit bijection in the reverse of mapsnf1o2 6670. (Contributed by
Stefan O'Rear, 24-Mar-2015.)
|
⊢ 𝑆 = {𝑋}
& ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) ⇒ ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑𝑚 𝑆) |
|
2.6.27 Infinite Cartesian products
|
|
Syntax | cixp 6672 |
Extend class notation to include infinite Cartesian products.
|
class X𝑥 ∈ 𝐴 𝐵 |
|
Definition | df-ixp 6673* |
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 6674* |
Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 6673, 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 6675* |
The value of an infinite Cartesian product with a singleton.
(Contributed by AV, 3-Dec-2018.)
|
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)}) |
|
Theorem | elixp2 6676* |
Membership in an infinite Cartesian product. See df-ixp 6673 for
discussion of the notation. (Contributed by NM, 28-Sep-2006.)
|
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | fvixp 6677* |
Projection of a factor of an indexed Cartesian product. (Contributed by
Mario Carneiro, 11-Jun-2016.)
|
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷) |
|
Theorem | ixpfn 6678* |
A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by
Mario Carneiro, 31-May-2014.)
|
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴) |
|
Theorem | elixp 6679* |
Membership in an infinite Cartesian product. (Contributed by NM,
28-Sep-2006.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | elixpconst 6680* |
Membership in an infinite Cartesian product of a constant 𝐵.
(Contributed by NM, 12-Apr-2008.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
|
Theorem | ixpconstg 6681* |
Infinite Cartesian product of a constant 𝐵. (Contributed by Mario
Carneiro, 11-Jan-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴)) |
|
Theorem | ixpconst 6682* |
Infinite Cartesian product of a constant 𝐵. (Contributed by NM,
28-Sep-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴) |
|
Theorem | ixpeq1 6683* |
Equality theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.)
|
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) |
|
Theorem | ixpeq1d 6684* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) |
|
Theorem | ss2ixp 6685 |
Subclass theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpeq2 6686 |
Equality theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpeq2dva 6687* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpeq2dv 6688* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | cbvixp 6689* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 20-Jun-2011.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
|
Theorem | cbvixpv 6690* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
|
Theorem | nfixpxy 6691* |
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 6692 |
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 6693* |
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 6694* |
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 6695* |
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 6696* |
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 6697* |
The intersection of two infinite Cartesian products. (Contributed by
Mario Carneiro, 3-Feb-2015.)
|
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpiinm 6698* |
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 6699* |
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 6700 |
An infinite Cartesian product with an empty index set. (Contributed by
NM, 21-Sep-2007.)
|
⊢ X𝑥 ∈ ∅ 𝐴 = {∅} |