Metamath Proof Explorer

Theorem tposf12

Description: Condition for an injective transposition. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tposf12 
|- ( Rel A -> ( F : A -1-1-> B -> tpos F : `' A -1-1-> B ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> F : A -1-1-> B )
2 relcnv 
 |-  Rel `' A
3 cnvf1o 
 |-  ( Rel `' A -> ( x e. `' A |-> U. `' { x } ) : `' A -1-1-onto-> `' `' A )
4 f1of1 
 |-  ( ( x e. `' A |-> U. `' { x } ) : `' A -1-1-onto-> `' `' A -> ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> `' `' A )
5 2 3 4 mp2b 
 |-  ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> `' `' A
6 simpl 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> Rel A )
7 dfrel2 
 |-  ( Rel A <-> `' `' A = A )
8 6 7 sylib 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> `' `' A = A )
9 f1eq3 
 |-  ( `' `' A = A -> ( ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> `' `' A <-> ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> A ) )
10 8 9 syl 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> ( ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> `' `' A <-> ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> A ) )
11 5 10 mpbii 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> A )
12 f1dm 
 |-  ( F : A -1-1-> B -> dom F = A )
13 1 12 syl 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> dom F = A )
14 13 cnveqd 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> `' dom F = `' A )
15 mpteq1 
 |-  ( `' dom F = `' A -> ( x e. `' dom F |-> U. `' { x } ) = ( x e. `' A |-> U. `' { x } ) )
16 f1eq1 
 |-  ( ( x e. `' dom F |-> U. `' { x } ) = ( x e. `' A |-> U. `' { x } ) -> ( ( x e. `' dom F |-> U. `' { x } ) : `' A -1-1-> A <-> ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> A ) )
17 14 15 16 3syl 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> ( ( x e. `' dom F |-> U. `' { x } ) : `' A -1-1-> A <-> ( x e. `' A |-> U. `' { x } ) : `' A -1-1-> A ) )
18 11 17 mpbird 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> ( x e. `' dom F |-> U. `' { x } ) : `' A -1-1-> A )
19 f1co 
 |-  ( ( F : A -1-1-> B /\ ( x e. `' dom F |-> U. `' { x } ) : `' A -1-1-> A ) -> ( F o. ( x e. `' dom F |-> U. `' { x } ) ) : `' A -1-1-> B )
20 1 18 19 syl2anc 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> ( F o. ( x e. `' dom F |-> U. `' { x } ) ) : `' A -1-1-> B )
21 12 releqd 
 |-  ( F : A -1-1-> B -> ( Rel dom F <-> Rel A ) )
22 21 biimparc 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> Rel dom F )
23 dftpos2 
 |-  ( Rel dom F -> tpos F = ( F o. ( x e. `' dom F |-> U. `' { x } ) ) )
24 f1eq1 
 |-  ( tpos F = ( F o. ( x e. `' dom F |-> U. `' { x } ) ) -> ( tpos F : `' A -1-1-> B <-> ( F o. ( x e. `' dom F |-> U. `' { x } ) ) : `' A -1-1-> B ) )
25 22 23 24 3syl 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> ( tpos F : `' A -1-1-> B <-> ( F o. ( x e. `' dom F |-> U. `' { x } ) ) : `' A -1-1-> B ) )
26 20 25 mpbird 
 |-  ( ( Rel A /\ F : A -1-1-> B ) -> tpos F : `' A -1-1-> B )
27 26 ex 
 |-  ( Rel A -> ( F : A -1-1-> B -> tpos F : `' A -1-1-> B ) )