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 ⊢ F = ran ⁡ x ∈ X ⟼ A B
flift.2 ⊢ φ ∧ x ∈ X → A ∈ R
flift.3 ⊢ φ ∧ x ∈ X → B ∈ S
Assertion fliftel1 ⊢ φ ∧ x ∈ X → A F B

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 opex ⊢ A B ∈ V
5 eqid ⊢ x ∈ X ⟼ A B = x ∈ X ⟼ A B
6 5 elrnmpt1 ⊢ x ∈ X ∧ A B ∈ V → A B ∈ ran ⁡ x ∈ X ⟼ A B
7 4 6 mpan2 ⊢ x ∈ X → A B ∈ ran ⁡ x ∈ X ⟼ A B
8 7 adantl ⊢ φ ∧ x ∈ X → A B ∈ ran ⁡ x ∈ X ⟼ A B
9 8 1 eleqtrrdi ⊢ φ ∧ x ∈ X → A B ∈ F
10 df-br ⊢ A F B ↔ A B ∈ F
11 9 10 sylibr ⊢ φ ∧ x ∈ X → A F B