Metamath Proof Explorer


Theorem brtpos2

Description: Value of the transposition at a pair <. A , B >. . (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion brtpos2
|- ( B e. V -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) )

Proof

Step Hyp Ref Expression
1 reltpos
 |-  Rel tpos F
2 1 brrelex1i
 |-  ( A tpos F B -> A e. _V )
3 2 a1i
 |-  ( B e. V -> ( A tpos F B -> A e. _V ) )
4 elex
 |-  ( A e. ( `' dom F u. { (/) } ) -> A e. _V )
5 4 adantr
 |-  ( ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) -> A e. _V )
6 5 a1i
 |-  ( B e. V -> ( ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) -> A e. _V ) )
7 df-tpos
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
8 7 breqi
 |-  ( A tpos F B <-> A ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) B )
9 brcog
 |-  ( ( A e. _V /\ B e. V ) -> ( A ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) B <-> E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) ) )
10 8 9 syl5bb
 |-  ( ( A e. _V /\ B e. V ) -> ( A tpos F B <-> E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) ) )
11 funmpt
 |-  Fun ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
12 funbrfv2b
 |-  ( Fun ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) -> ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) ) )
13 11 12 ax-mp
 |-  ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) )
14 snex
 |-  { x } e. _V
15 14 cnvex
 |-  `' { x } e. _V
16 15 uniex
 |-  U. `' { x } e. _V
17 eqid
 |-  ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
18 16 17 dmmpti
 |-  dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( `' dom F u. { (/) } )
19 18 eleq2i
 |-  ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) <-> A e. ( `' dom F u. { (/) } ) )
20 eqcom
 |-  ( ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y <-> y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) )
21 19 20 anbi12i
 |-  ( ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) <-> ( A e. ( `' dom F u. { (/) } ) /\ y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) ) )
22 sneq
 |-  ( x = A -> { x } = { A } )
23 22 cnveqd
 |-  ( x = A -> `' { x } = `' { A } )
24 23 unieqd
 |-  ( x = A -> U. `' { x } = U. `' { A } )
25 snex
 |-  { A } e. _V
26 25 cnvex
 |-  `' { A } e. _V
27 26 uniex
 |-  U. `' { A } e. _V
28 24 17 27 fvmpt
 |-  ( A e. ( `' dom F u. { (/) } ) -> ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = U. `' { A } )
29 28 eqeq2d
 |-  ( A e. ( `' dom F u. { (/) } ) -> ( y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) <-> y = U. `' { A } ) )
30 29 pm5.32i
 |-  ( ( A e. ( `' dom F u. { (/) } ) /\ y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) ) <-> ( A e. ( `' dom F u. { (/) } ) /\ y = U. `' { A } ) )
31 21 30 bitri
 |-  ( ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) <-> ( A e. ( `' dom F u. { (/) } ) /\ y = U. `' { A } ) )
32 13 31 bitri
 |-  ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( A e. ( `' dom F u. { (/) } ) /\ y = U. `' { A } ) )
33 32 biancomi
 |-  ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( y = U. `' { A } /\ A e. ( `' dom F u. { (/) } ) ) )
34 33 anbi1i
 |-  ( ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> ( ( y = U. `' { A } /\ A e. ( `' dom F u. { (/) } ) ) /\ y F B ) )
35 anass
 |-  ( ( ( y = U. `' { A } /\ A e. ( `' dom F u. { (/) } ) ) /\ y F B ) <-> ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) )
36 34 35 bitri
 |-  ( ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) )
37 36 exbii
 |-  ( E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> E. y ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) )
38 breq1
 |-  ( y = U. `' { A } -> ( y F B <-> U. `' { A } F B ) )
39 38 anbi2d
 |-  ( y = U. `' { A } -> ( ( A e. ( `' dom F u. { (/) } ) /\ y F B ) <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) )
40 27 39 ceqsexv
 |-  ( E. y ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) )
41 37 40 bitri
 |-  ( E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) )
42 10 41 bitrdi
 |-  ( ( A e. _V /\ B e. V ) -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) )
43 42 expcom
 |-  ( B e. V -> ( A e. _V -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) ) )
44 3 6 43 pm5.21ndd
 |-  ( B e. V -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) )