Metamath Proof Explorer


Theorem tpostpos

Description: Value of the double transposition for a general class F . (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion tpostpos
|- tpos tpos F = ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )

Proof

Step Hyp Ref Expression
1 reltpos
 |-  Rel tpos tpos F
2 relinxp
 |-  Rel ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
3 relcnv
 |-  Rel `' dom tpos F
4 df-rel
 |-  ( Rel `' dom tpos F <-> `' dom tpos F C_ ( _V X. _V ) )
5 3 4 mpbi
 |-  `' dom tpos F C_ ( _V X. _V )
6 simpl
 |-  ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) -> w e. `' dom tpos F )
7 5 6 sselid
 |-  ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) -> w e. ( _V X. _V ) )
8 simpr
 |-  ( ( w F z /\ w e. ( _V X. _V ) ) -> w e. ( _V X. _V ) )
9 elvv
 |-  ( w e. ( _V X. _V ) <-> E. x E. y w = <. x , y >. )
10 eleq1
 |-  ( w = <. x , y >. -> ( w e. `' dom tpos F <-> <. x , y >. e. `' dom tpos F ) )
11 vex
 |-  x e. _V
12 vex
 |-  y e. _V
13 11 12 opelcnv
 |-  ( <. x , y >. e. `' dom tpos F <-> <. y , x >. e. dom tpos F )
14 10 13 bitrdi
 |-  ( w = <. x , y >. -> ( w e. `' dom tpos F <-> <. y , x >. e. dom tpos F ) )
15 sneq
 |-  ( w = <. x , y >. -> { w } = { <. x , y >. } )
16 15 cnveqd
 |-  ( w = <. x , y >. -> `' { w } = `' { <. x , y >. } )
17 16 unieqd
 |-  ( w = <. x , y >. -> U. `' { w } = U. `' { <. x , y >. } )
18 opswap
 |-  U. `' { <. x , y >. } = <. y , x >.
19 17 18 eqtrdi
 |-  ( w = <. x , y >. -> U. `' { w } = <. y , x >. )
20 19 breq1d
 |-  ( w = <. x , y >. -> ( U. `' { w } tpos F z <-> <. y , x >. tpos F z ) )
21 14 20 anbi12d
 |-  ( w = <. x , y >. -> ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) <-> ( <. y , x >. e. dom tpos F /\ <. y , x >. tpos F z ) ) )
22 opex
 |-  <. y , x >. e. _V
23 vex
 |-  z e. _V
24 22 23 breldm
 |-  ( <. y , x >. tpos F z -> <. y , x >. e. dom tpos F )
25 24 pm4.71ri
 |-  ( <. y , x >. tpos F z <-> ( <. y , x >. e. dom tpos F /\ <. y , x >. tpos F z ) )
26 brtpos
 |-  ( z e. _V -> ( <. y , x >. tpos F z <-> <. x , y >. F z ) )
27 26 elv
 |-  ( <. y , x >. tpos F z <-> <. x , y >. F z )
28 25 27 bitr3i
 |-  ( ( <. y , x >. e. dom tpos F /\ <. y , x >. tpos F z ) <-> <. x , y >. F z )
29 21 28 bitrdi
 |-  ( w = <. x , y >. -> ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) <-> <. x , y >. F z ) )
30 breq1
 |-  ( w = <. x , y >. -> ( w F z <-> <. x , y >. F z ) )
31 29 30 bitr4d
 |-  ( w = <. x , y >. -> ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) <-> w F z ) )
32 31 exlimivv
 |-  ( E. x E. y w = <. x , y >. -> ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) <-> w F z ) )
33 9 32 sylbi
 |-  ( w e. ( _V X. _V ) -> ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) <-> w F z ) )
34 iba
 |-  ( w e. ( _V X. _V ) -> ( w F z <-> ( w F z /\ w e. ( _V X. _V ) ) ) )
35 33 34 bitrd
 |-  ( w e. ( _V X. _V ) -> ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) <-> ( w F z /\ w e. ( _V X. _V ) ) ) )
36 7 8 35 pm5.21nii
 |-  ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) <-> ( w F z /\ w e. ( _V X. _V ) ) )
37 elsni
 |-  ( w e. { (/) } -> w = (/) )
38 37 sneqd
 |-  ( w e. { (/) } -> { w } = { (/) } )
39 38 cnveqd
 |-  ( w e. { (/) } -> `' { w } = `' { (/) } )
40 cnvsn0
 |-  `' { (/) } = (/)
41 39 40 eqtrdi
 |-  ( w e. { (/) } -> `' { w } = (/) )
42 41 unieqd
 |-  ( w e. { (/) } -> U. `' { w } = U. (/) )
43 uni0
 |-  U. (/) = (/)
44 42 43 eqtrdi
 |-  ( w e. { (/) } -> U. `' { w } = (/) )
45 44 breq1d
 |-  ( w e. { (/) } -> ( U. `' { w } tpos F z <-> (/) tpos F z ) )
46 brtpos0
 |-  ( z e. _V -> ( (/) tpos F z <-> (/) F z ) )
47 46 elv
 |-  ( (/) tpos F z <-> (/) F z )
48 45 47 bitrdi
 |-  ( w e. { (/) } -> ( U. `' { w } tpos F z <-> (/) F z ) )
49 37 breq1d
 |-  ( w e. { (/) } -> ( w F z <-> (/) F z ) )
50 48 49 bitr4d
 |-  ( w e. { (/) } -> ( U. `' { w } tpos F z <-> w F z ) )
51 50 pm5.32i
 |-  ( ( w e. { (/) } /\ U. `' { w } tpos F z ) <-> ( w e. { (/) } /\ w F z ) )
52 51 biancomi
 |-  ( ( w e. { (/) } /\ U. `' { w } tpos F z ) <-> ( w F z /\ w e. { (/) } ) )
53 36 52 orbi12i
 |-  ( ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) \/ ( w e. { (/) } /\ U. `' { w } tpos F z ) ) <-> ( ( w F z /\ w e. ( _V X. _V ) ) \/ ( w F z /\ w e. { (/) } ) ) )
54 andir
 |-  ( ( ( w e. `' dom tpos F \/ w e. { (/) } ) /\ U. `' { w } tpos F z ) <-> ( ( w e. `' dom tpos F /\ U. `' { w } tpos F z ) \/ ( w e. { (/) } /\ U. `' { w } tpos F z ) ) )
55 andi
 |-  ( ( w F z /\ ( w e. ( _V X. _V ) \/ w e. { (/) } ) ) <-> ( ( w F z /\ w e. ( _V X. _V ) ) \/ ( w F z /\ w e. { (/) } ) ) )
56 53 54 55 3bitr4i
 |-  ( ( ( w e. `' dom tpos F \/ w e. { (/) } ) /\ U. `' { w } tpos F z ) <-> ( w F z /\ ( w e. ( _V X. _V ) \/ w e. { (/) } ) ) )
57 elun
 |-  ( w e. ( `' dom tpos F u. { (/) } ) <-> ( w e. `' dom tpos F \/ w e. { (/) } ) )
58 57 anbi1i
 |-  ( ( w e. ( `' dom tpos F u. { (/) } ) /\ U. `' { w } tpos F z ) <-> ( ( w e. `' dom tpos F \/ w e. { (/) } ) /\ U. `' { w } tpos F z ) )
59 brxp
 |-  ( w ( ( ( _V X. _V ) u. { (/) } ) X. _V ) z <-> ( w e. ( ( _V X. _V ) u. { (/) } ) /\ z e. _V ) )
60 23 59 mpbiran2
 |-  ( w ( ( ( _V X. _V ) u. { (/) } ) X. _V ) z <-> w e. ( ( _V X. _V ) u. { (/) } ) )
61 elun
 |-  ( w e. ( ( _V X. _V ) u. { (/) } ) <-> ( w e. ( _V X. _V ) \/ w e. { (/) } ) )
62 60 61 bitri
 |-  ( w ( ( ( _V X. _V ) u. { (/) } ) X. _V ) z <-> ( w e. ( _V X. _V ) \/ w e. { (/) } ) )
63 62 anbi2i
 |-  ( ( w F z /\ w ( ( ( _V X. _V ) u. { (/) } ) X. _V ) z ) <-> ( w F z /\ ( w e. ( _V X. _V ) \/ w e. { (/) } ) ) )
64 56 58 63 3bitr4i
 |-  ( ( w e. ( `' dom tpos F u. { (/) } ) /\ U. `' { w } tpos F z ) <-> ( w F z /\ w ( ( ( _V X. _V ) u. { (/) } ) X. _V ) z ) )
65 brtpos2
 |-  ( z e. _V -> ( w tpos tpos F z <-> ( w e. ( `' dom tpos F u. { (/) } ) /\ U. `' { w } tpos F z ) ) )
66 65 elv
 |-  ( w tpos tpos F z <-> ( w e. ( `' dom tpos F u. { (/) } ) /\ U. `' { w } tpos F z ) )
67 brin
 |-  ( w ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) ) z <-> ( w F z /\ w ( ( ( _V X. _V ) u. { (/) } ) X. _V ) z ) )
68 64 66 67 3bitr4i
 |-  ( w tpos tpos F z <-> w ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) ) z )
69 1 2 68 eqbrriv
 |-  tpos tpos F = ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )