Step |
Hyp |
Ref |
Expression |
1 |
|
reltpos |
|- Rel tpos F |
2 |
1
|
brrelex1i |
|- ( A tpos F B -> A e. _V ) |
3 |
2
|
a1i |
|- ( B e. V -> ( A tpos F B -> A e. _V ) ) |
4 |
|
elex |
|- ( A e. ( `' dom F u. { (/) } ) -> A e. _V ) |
5 |
4
|
adantr |
|- ( ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) -> A e. _V ) |
6 |
5
|
a1i |
|- ( B e. V -> ( ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) -> A e. _V ) ) |
7 |
|
df-tpos |
|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) |
8 |
7
|
breqi |
|- ( A tpos F B <-> A ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) B ) |
9 |
|
brcog |
|- ( ( A e. _V /\ B e. V ) -> ( A ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) B <-> E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) ) ) |
10 |
8 9
|
syl5bb |
|- ( ( A e. _V /\ B e. V ) -> ( A tpos F B <-> E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) ) ) |
11 |
|
funmpt |
|- Fun ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |
12 |
|
funbrfv2b |
|- ( Fun ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) -> ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) ) ) |
13 |
11 12
|
ax-mp |
|- ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) ) |
14 |
|
snex |
|- { x } e. _V |
15 |
14
|
cnvex |
|- `' { x } e. _V |
16 |
15
|
uniex |
|- U. `' { x } e. _V |
17 |
|
eqid |
|- ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |
18 |
16 17
|
dmmpti |
|- dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( `' dom F u. { (/) } ) |
19 |
18
|
eleq2i |
|- ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) <-> A e. ( `' dom F u. { (/) } ) ) |
20 |
|
eqcom |
|- ( ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y <-> y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) ) |
21 |
19 20
|
anbi12i |
|- ( ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) <-> ( A e. ( `' dom F u. { (/) } ) /\ y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) ) ) |
22 |
|
sneq |
|- ( x = A -> { x } = { A } ) |
23 |
22
|
cnveqd |
|- ( x = A -> `' { x } = `' { A } ) |
24 |
23
|
unieqd |
|- ( x = A -> U. `' { x } = U. `' { A } ) |
25 |
|
snex |
|- { A } e. _V |
26 |
25
|
cnvex |
|- `' { A } e. _V |
27 |
26
|
uniex |
|- U. `' { A } e. _V |
28 |
24 17 27
|
fvmpt |
|- ( A e. ( `' dom F u. { (/) } ) -> ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = U. `' { A } ) |
29 |
28
|
eqeq2d |
|- ( A e. ( `' dom F u. { (/) } ) -> ( y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) <-> y = U. `' { A } ) ) |
30 |
29
|
pm5.32i |
|- ( ( A e. ( `' dom F u. { (/) } ) /\ y = ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) ) <-> ( A e. ( `' dom F u. { (/) } ) /\ y = U. `' { A } ) ) |
31 |
21 30
|
bitri |
|- ( ( A e. dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) /\ ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ` A ) = y ) <-> ( A e. ( `' dom F u. { (/) } ) /\ y = U. `' { A } ) ) |
32 |
13 31
|
bitri |
|- ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( A e. ( `' dom F u. { (/) } ) /\ y = U. `' { A } ) ) |
33 |
32
|
biancomi |
|- ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y <-> ( y = U. `' { A } /\ A e. ( `' dom F u. { (/) } ) ) ) |
34 |
33
|
anbi1i |
|- ( ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> ( ( y = U. `' { A } /\ A e. ( `' dom F u. { (/) } ) ) /\ y F B ) ) |
35 |
|
anass |
|- ( ( ( y = U. `' { A } /\ A e. ( `' dom F u. { (/) } ) ) /\ y F B ) <-> ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) ) |
36 |
34 35
|
bitri |
|- ( ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) ) |
37 |
36
|
exbii |
|- ( E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> E. y ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) ) |
38 |
|
breq1 |
|- ( y = U. `' { A } -> ( y F B <-> U. `' { A } F B ) ) |
39 |
38
|
anbi2d |
|- ( y = U. `' { A } -> ( ( A e. ( `' dom F u. { (/) } ) /\ y F B ) <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) ) |
40 |
27 39
|
ceqsexv |
|- ( E. y ( y = U. `' { A } /\ ( A e. ( `' dom F u. { (/) } ) /\ y F B ) ) <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) |
41 |
37 40
|
bitri |
|- ( E. y ( A ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) y /\ y F B ) <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) |
42 |
10 41
|
bitrdi |
|- ( ( A e. _V /\ B e. V ) -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) ) |
43 |
42
|
expcom |
|- ( B e. V -> ( A e. _V -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) ) ) |
44 |
3 6 43
|
pm5.21ndd |
|- ( B e. V -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) ) |