Metamath Proof Explorer


Theorem dftpos4

Description: Alternate definition of tpos . (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion dftpos4
|- tpos F = ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )

Proof

Step Hyp Ref Expression
1 df-tpos
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
2 relcnv
 |-  Rel `' dom F
3 df-rel
 |-  ( Rel `' dom F <-> `' dom F C_ ( _V X. _V ) )
4 2 3 mpbi
 |-  `' dom F C_ ( _V X. _V )
5 unss1
 |-  ( `' dom F C_ ( _V X. _V ) -> ( `' dom F u. { (/) } ) C_ ( ( _V X. _V ) u. { (/) } ) )
6 resmpt
 |-  ( ( `' dom F u. { (/) } ) C_ ( ( _V X. _V ) u. { (/) } ) -> ( ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) |` ( `' dom F u. { (/) } ) ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
7 4 5 6 mp2b
 |-  ( ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) |` ( `' dom F u. { (/) } ) ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
8 resss
 |-  ( ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) |` ( `' dom F u. { (/) } ) ) C_ ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } )
9 7 8 eqsstrri
 |-  ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } )
10 coss2
 |-  ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) -> ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) )
11 9 10 ax-mp
 |-  ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
12 1 11 eqsstri
 |-  tpos F C_ ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
13 relco
 |-  Rel ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
14 vex
 |-  y e. _V
15 vex
 |-  z e. _V
16 14 15 opelco
 |-  ( <. y , z >. e. ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) <-> E. w ( y ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) w /\ w F z ) )
17 vex
 |-  w e. _V
18 eleq1
 |-  ( x = y -> ( x e. ( ( _V X. _V ) u. { (/) } ) <-> y e. ( ( _V X. _V ) u. { (/) } ) ) )
19 sneq
 |-  ( x = y -> { x } = { y } )
20 19 cnveqd
 |-  ( x = y -> `' { x } = `' { y } )
21 20 unieqd
 |-  ( x = y -> U. `' { x } = U. `' { y } )
22 21 eqeq2d
 |-  ( x = y -> ( z = U. `' { x } <-> z = U. `' { y } ) )
23 18 22 anbi12d
 |-  ( x = y -> ( ( x e. ( ( _V X. _V ) u. { (/) } ) /\ z = U. `' { x } ) <-> ( y e. ( ( _V X. _V ) u. { (/) } ) /\ z = U. `' { y } ) ) )
24 eqeq1
 |-  ( z = w -> ( z = U. `' { y } <-> w = U. `' { y } ) )
25 24 anbi2d
 |-  ( z = w -> ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ z = U. `' { y } ) <-> ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) ) )
26 df-mpt
 |-  ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) = { <. x , z >. | ( x e. ( ( _V X. _V ) u. { (/) } ) /\ z = U. `' { x } ) }
27 14 17 23 25 26 brab
 |-  ( y ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) w <-> ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) )
28 simplr
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> w = U. `' { y } )
29 17 15 breldm
 |-  ( w F z -> w e. dom F )
30 29 adantl
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> w e. dom F )
31 28 30 eqeltrrd
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> U. `' { y } e. dom F )
32 elvv
 |-  ( y e. ( _V X. _V ) <-> E. z E. w y = <. z , w >. )
33 opswap
 |-  U. `' { <. z , w >. } = <. w , z >.
34 33 eleq1i
 |-  ( U. `' { <. z , w >. } e. dom F <-> <. w , z >. e. dom F )
35 15 17 opelcnv
 |-  ( <. z , w >. e. `' dom F <-> <. w , z >. e. dom F )
36 34 35 bitr4i
 |-  ( U. `' { <. z , w >. } e. dom F <-> <. z , w >. e. `' dom F )
37 sneq
 |-  ( y = <. z , w >. -> { y } = { <. z , w >. } )
38 37 cnveqd
 |-  ( y = <. z , w >. -> `' { y } = `' { <. z , w >. } )
39 38 unieqd
 |-  ( y = <. z , w >. -> U. `' { y } = U. `' { <. z , w >. } )
40 39 eleq1d
 |-  ( y = <. z , w >. -> ( U. `' { y } e. dom F <-> U. `' { <. z , w >. } e. dom F ) )
41 eleq1
 |-  ( y = <. z , w >. -> ( y e. `' dom F <-> <. z , w >. e. `' dom F ) )
42 40 41 bibi12d
 |-  ( y = <. z , w >. -> ( ( U. `' { y } e. dom F <-> y e. `' dom F ) <-> ( U. `' { <. z , w >. } e. dom F <-> <. z , w >. e. `' dom F ) ) )
43 36 42 mpbiri
 |-  ( y = <. z , w >. -> ( U. `' { y } e. dom F <-> y e. `' dom F ) )
44 43 exlimivv
 |-  ( E. z E. w y = <. z , w >. -> ( U. `' { y } e. dom F <-> y e. `' dom F ) )
45 32 44 sylbi
 |-  ( y e. ( _V X. _V ) -> ( U. `' { y } e. dom F <-> y e. `' dom F ) )
46 45 biimpcd
 |-  ( U. `' { y } e. dom F -> ( y e. ( _V X. _V ) -> y e. `' dom F ) )
47 elun1
 |-  ( y e. `' dom F -> y e. ( `' dom F u. { (/) } ) )
48 46 47 syl6
 |-  ( U. `' { y } e. dom F -> ( y e. ( _V X. _V ) -> y e. ( `' dom F u. { (/) } ) ) )
49 31 48 syl
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> ( y e. ( _V X. _V ) -> y e. ( `' dom F u. { (/) } ) ) )
50 elun2
 |-  ( y e. { (/) } -> y e. ( `' dom F u. { (/) } ) )
51 50 a1i
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> ( y e. { (/) } -> y e. ( `' dom F u. { (/) } ) ) )
52 simpll
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> y e. ( ( _V X. _V ) u. { (/) } ) )
53 elun
 |-  ( y e. ( ( _V X. _V ) u. { (/) } ) <-> ( y e. ( _V X. _V ) \/ y e. { (/) } ) )
54 52 53 sylib
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> ( y e. ( _V X. _V ) \/ y e. { (/) } ) )
55 49 51 54 mpjaod
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> y e. ( `' dom F u. { (/) } ) )
56 simpr
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> w F z )
57 28 56 eqbrtrrd
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> U. `' { y } F z )
58 55 57 jca
 |-  ( ( ( y e. ( ( _V X. _V ) u. { (/) } ) /\ w = U. `' { y } ) /\ w F z ) -> ( y e. ( `' dom F u. { (/) } ) /\ U. `' { y } F z ) )
59 27 58 sylanb
 |-  ( ( y ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) w /\ w F z ) -> ( y e. ( `' dom F u. { (/) } ) /\ U. `' { y } F z ) )
60 brtpos2
 |-  ( z e. _V -> ( y tpos F z <-> ( y e. ( `' dom F u. { (/) } ) /\ U. `' { y } F z ) ) )
61 15 60 ax-mp
 |-  ( y tpos F z <-> ( y e. ( `' dom F u. { (/) } ) /\ U. `' { y } F z ) )
62 59 61 sylibr
 |-  ( ( y ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) w /\ w F z ) -> y tpos F z )
63 df-br
 |-  ( y tpos F z <-> <. y , z >. e. tpos F )
64 62 63 sylib
 |-  ( ( y ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) w /\ w F z ) -> <. y , z >. e. tpos F )
65 64 exlimiv
 |-  ( E. w ( y ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) w /\ w F z ) -> <. y , z >. e. tpos F )
66 16 65 sylbi
 |-  ( <. y , z >. e. ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) -> <. y , z >. e. tpos F )
67 13 66 relssi
 |-  ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) C_ tpos F
68 12 67 eqssi
 |-  tpos F = ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )