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

Metamath Proof Explorer

Theorem fliftel1

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion fliftel1 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 𝐹 𝐵 )

Proof

Step Hyp Ref Expression
1 flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2 flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3 flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
6 5 elrnmpt1 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
7 4 6 mpan2 ⊢ ( 𝑥 ∈ 𝑋 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
9 8 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 )
10 df-br ⊢ ( 𝐴 𝐹 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 )
11 9 10 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 𝐹 𝐵 )