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 } ) )