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 e. X |-> <. A , B >. )
flift.2 
|- ( ( ph /\ x e. X ) -> A e. R )
flift.3 
|- ( ( ph /\ x e. X ) -> B e. S )
Assertion fliftel1 
|- ( ( ph /\ x e. X ) -> A F B )

Proof

Step Hyp Ref Expression
1 flift.1 
 |-  F = ran ( x e. X |-> <. A , B >. )
2 flift.2 
 |-  ( ( ph /\ x e. X ) -> A e. R )
3 flift.3 
 |-  ( ( ph /\ x e. X ) -> B e. S )
4 opex 
 |-  <. A , B >. e. _V
5 eqid 
 |-  ( x e. X |-> <. A , B >. ) = ( x e. X |-> <. A , B >. )
6 5 elrnmpt1 
 |-  ( ( x e. X /\ <. A , B >. e. _V ) -> <. A , B >. e. ran ( x e. X |-> <. A , B >. ) )
7 4 6 mpan2 
 |-  ( x e. X -> <. A , B >. e. ran ( x e. X |-> <. A , B >. ) )
8 7 adantl 
 |-  ( ( ph /\ x e. X ) -> <. A , B >. e. ran ( x e. X |-> <. A , B >. ) )
9 8 1 eleqtrrdi 
 |-  ( ( ph /\ x e. X ) -> <. A , B >. e. F )
10 df-br 
 |-  ( A F B <-> <. A , B >. e. F )
11 9 10 sylibr 
 |-  ( ( ph /\ x e. X ) -> A F B )