Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | offval.1 | ⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) | |
| offval.2 | ⊢ ( 𝜑 → 𝐺 Fn 𝐵 ) | ||
| offval.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | ||
| offval.4 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | ||
| offval.5 | ⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆 | ||
| offval.6 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 ) | ||
| offval.7 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = 𝐷 ) | ||
| Assertion | ofrfval | ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝑆 𝐶 𝑅 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | offval.1 | ⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) | |
| 2 | offval.2 | ⊢ ( 𝜑 → 𝐺 Fn 𝐵 ) | |
| 3 | offval.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
| 4 | offval.4 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | |
| 5 | offval.5 | ⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆 | |
| 6 | offval.6 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 ) | |
| 7 | offval.7 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = 𝐷 ) | |
| 8 | 1 3 | fnexd | ⊢ ( 𝜑 → 𝐹 ∈ V ) |
| 9 | 2 4 | fnexd | ⊢ ( 𝜑 → 𝐺 ∈ V ) |
| 10 | 1 2 8 9 5 6 7 | ofrfvalg | ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝑆 𝐶 𝑅 𝐷 ) ) |