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 >. ) )