Step |
Hyp |
Ref |
Expression |
1 |
|
brtpos2 |
|- ( A e. V -> ( (/) tpos F A <-> ( (/) e. ( `' dom F u. { (/) } ) /\ U. `' { (/) } F A ) ) ) |
2 |
|
ssun2 |
|- { (/) } C_ ( `' dom F u. { (/) } ) |
3 |
|
0ex |
|- (/) e. _V |
4 |
3
|
snid |
|- (/) e. { (/) } |
5 |
2 4
|
sselii |
|- (/) e. ( `' dom F u. { (/) } ) |
6 |
5
|
biantrur |
|- ( U. `' { (/) } F A <-> ( (/) e. ( `' dom F u. { (/) } ) /\ U. `' { (/) } F A ) ) |
7 |
|
cnvsn0 |
|- `' { (/) } = (/) |
8 |
7
|
unieqi |
|- U. `' { (/) } = U. (/) |
9 |
|
uni0 |
|- U. (/) = (/) |
10 |
8 9
|
eqtri |
|- U. `' { (/) } = (/) |
11 |
10
|
breq1i |
|- ( U. `' { (/) } F A <-> (/) F A ) |
12 |
6 11
|
bitr3i |
|- ( ( (/) e. ( `' dom F u. { (/) } ) /\ U. `' { (/) } F A ) <-> (/) F A ) |
13 |
1 12
|
bitrdi |
|- ( A e. V -> ( (/) tpos F A <-> (/) F A ) ) |