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

Metamath Proof Explorer

Theorem fliftcnv

Description: Converse of 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 fliftcnv 
|- ( ph -> `' F = ran ( x e. X |-> <. B , A >. ) )

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 eqid 
 |-  ran ( x e. X |-> <. B , A >. ) = ran ( x e. X |-> <. B , A >. )
5 4 3 2 fliftrel 
 |-  ( ph -> ran ( x e. X |-> <. B , A >. ) C_ ( S X. R ) )
6 relxp 
 |-  Rel ( S X. R )
7 relss 
 |-  ( ran ( x e. X |-> <. B , A >. ) C_ ( S X. R ) -> ( Rel ( S X. R ) -> Rel ran ( x e. X |-> <. B , A >. ) ) )
8 5 6 7 mpisyl 
 |-  ( ph -> Rel ran ( x e. X |-> <. B , A >. ) )
9 relcnv 
 |-  Rel `' F
10 8 9 jctil 
 |-  ( ph -> ( Rel `' F /\ Rel ran ( x e. X |-> <. B , A >. ) ) )
11 1 2 3 fliftel 
 |-  ( ph -> ( z F y <-> E. x e. X ( z = A /\ y = B ) ) )
12 vex 
 |-  y e. _V
13 vex 
 |-  z e. _V
14 12 13 brcnv 
 |-  ( y `' F z <-> z F y )
15 ancom 
 |-  ( ( y = B /\ z = A ) <-> ( z = A /\ y = B ) )
16 15 rexbii 
 |-  ( E. x e. X ( y = B /\ z = A ) <-> E. x e. X ( z = A /\ y = B ) )
17 11 14 16 3bitr4g 
 |-  ( ph -> ( y `' F z <-> E. x e. X ( y = B /\ z = A ) ) )
18 4 3 2 fliftel 
 |-  ( ph -> ( y ran ( x e. X |-> <. B , A >. ) z <-> E. x e. X ( y = B /\ z = A ) ) )
19 17 18 bitr4d 
 |-  ( ph -> ( y `' F z <-> y ran ( x e. X |-> <. B , A >. ) z ) )
20 df-br 
 |-  ( y `' F z <-> <. y , z >. e. `' F )
21 df-br 
 |-  ( y ran ( x e. X |-> <. B , A >. ) z <-> <. y , z >. e. ran ( x e. X |-> <. B , A >. ) )
22 19 20 21 3bitr3g 
 |-  ( ph -> ( <. y , z >. e. `' F <-> <. y , z >. e. ran ( x e. X |-> <. B , A >. ) ) )
23 22 eqrelrdv2 
 |-  ( ( ( Rel `' F /\ Rel ran ( x e. X |-> <. B , A >. ) ) /\ ph ) -> `' F = ran ( x e. X |-> <. B , A >. ) )
24 10 23 mpancom 
 |-  ( ph -> `' F = ran ( x e. X |-> <. B , A >. ) )