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 bitrid 
 |-  ( ( 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 ) ) )