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