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	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
	flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
	flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion	fliftrel	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑅 × 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		flift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2		flift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3		flift.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4	2 3	opelxpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) )
5	4	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) : 𝑋 ⟶ ( 𝑅 × 𝑆 ) )
6	5	frnd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ⊆ ( 𝑅 × 𝑆 ) )
7	1 6	eqsstrid	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑅 × 𝑆 ) )