Step |
Hyp |
Ref |
Expression |
1 |
|
fneqeql |
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> dom ( F i^i G ) = A ) ) |
2 |
|
eqss |
|- ( dom ( F i^i G ) = A <-> ( dom ( F i^i G ) C_ A /\ A C_ dom ( F i^i G ) ) ) |
3 |
|
inss1 |
|- ( F i^i G ) C_ F |
4 |
|
dmss |
|- ( ( F i^i G ) C_ F -> dom ( F i^i G ) C_ dom F ) |
5 |
3 4
|
ax-mp |
|- dom ( F i^i G ) C_ dom F |
6 |
|
fndm |
|- ( F Fn A -> dom F = A ) |
7 |
6
|
adantr |
|- ( ( F Fn A /\ G Fn A ) -> dom F = A ) |
8 |
5 7
|
sseqtrid |
|- ( ( F Fn A /\ G Fn A ) -> dom ( F i^i G ) C_ A ) |
9 |
8
|
biantrurd |
|- ( ( F Fn A /\ G Fn A ) -> ( A C_ dom ( F i^i G ) <-> ( dom ( F i^i G ) C_ A /\ A C_ dom ( F i^i G ) ) ) ) |
10 |
2 9
|
bitr4id |
|- ( ( F Fn A /\ G Fn A ) -> ( dom ( F i^i G ) = A <-> A C_ dom ( F i^i G ) ) ) |
11 |
1 10
|
bitrd |
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A C_ dom ( F i^i G ) ) ) |