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