This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fliftrel

Description: F , a function lift, is a subset of R X. S . (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 ⊢ F = ran ⁡ x ∈ X ⟼ A B
flift.2 ⊢ φ ∧ x ∈ X → A ∈ R
flift.3 ⊢ φ ∧ x ∈ X → B ∈ S
Assertion fliftrel ⊢ φ → F ⊆ R × S

Proof

Step Hyp Ref Expression
1 flift.1 ⊢ F = ran ⁡ x ∈ X ⟼ A B
2 flift.2 ⊢ φ ∧ x ∈ X → A ∈ R
3 flift.3 ⊢ φ ∧ x ∈ X → B ∈ S
4 2 3 opelxpd ⊢ φ ∧ x ∈ X → A B ∈ R × S
5 4 fmpttd ⊢ φ → x ∈ X ⟼ A B : X ⟶ R × S
6 5 frnd ⊢ φ → ran ⁡ x ∈ X ⟼ A B ⊆ R × S
7 1 6 eqsstrid ⊢ φ → F ⊆ R × S