Description: Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eropr2.1 | ⊢ 𝐽 = ( 𝐴 / ∼ ) | |
eropr2.2 | ⊢ ⨣ = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑥 = [ 𝑝 ] ∼ ∧ 𝑦 = [ 𝑞 ] ∼ ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] ∼ ) } | ||
eropr2.3 | ⊢ ( 𝜑 → ∼ ∈ 𝑋 ) | ||
eropr2.4 | ⊢ ( 𝜑 → ∼ Er 𝑈 ) | ||
eropr2.5 | ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 ) | ||
eropr2.6 | ⊢ ( 𝜑 → + : ( 𝐴 × 𝐴 ) ⟶ 𝐴 ) | ||
eropr2.7 | ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) ) → ( ( 𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢 ) → ( 𝑟 + 𝑡 ) ∼ ( 𝑠 + 𝑢 ) ) ) | ||
Assertion | eroprf2 | ⊢ ( 𝜑 → ⨣ : ( 𝐽 × 𝐽 ) ⟶ 𝐽 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eropr2.1 | ⊢ 𝐽 = ( 𝐴 / ∼ ) | |
2 | eropr2.2 | ⊢ ⨣ = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑥 = [ 𝑝 ] ∼ ∧ 𝑦 = [ 𝑞 ] ∼ ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] ∼ ) } | |
3 | eropr2.3 | ⊢ ( 𝜑 → ∼ ∈ 𝑋 ) | |
4 | eropr2.4 | ⊢ ( 𝜑 → ∼ Er 𝑈 ) | |
5 | eropr2.5 | ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 ) | |
6 | eropr2.6 | ⊢ ( 𝜑 → + : ( 𝐴 × 𝐴 ) ⟶ 𝐴 ) | |
7 | eropr2.7 | ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) ) → ( ( 𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢 ) → ( 𝑟 + 𝑡 ) ∼ ( 𝑠 + 𝑢 ) ) ) | |
8 | 1 1 3 4 4 4 5 5 5 6 7 2 3 3 1 | eroprf | ⊢ ( 𝜑 → ⨣ : ( 𝐽 × 𝐽 ) ⟶ 𝐽 ) |