Description: Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 7-Aug-2014) (Proof shortened by Mario Carneiro, 24-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | relmptopab.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } ) | |
| Assertion | relmptopab | ⊢ Rel ( 𝐹 ‘ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relmptopab.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } ) | |
| 2 | 1 | fvmptss | ⊢ ( ∀ 𝑥 ∈ 𝐴 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } ⊆ ( V × V ) → ( 𝐹 ‘ 𝐵 ) ⊆ ( V × V ) ) |
| 3 | relopab | ⊢ Rel { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } | |
| 4 | df-rel | ⊢ ( Rel { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } ↔ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } ⊆ ( V × V ) ) | |
| 5 | 3 4 | mpbi | ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } ⊆ ( V × V ) |
| 6 | 5 | a1i | ⊢ ( 𝑥 ∈ 𝐴 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } ⊆ ( V × V ) ) |
| 7 | 2 6 | mprg | ⊢ ( 𝐹 ‘ 𝐵 ) ⊆ ( V × V ) |
| 8 | df-rel | ⊢ ( Rel ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊆ ( V × V ) ) | |
| 9 | 7 8 | mpbir | ⊢ Rel ( 𝐹 ‘ 𝐵 ) |