Step |
Hyp |
Ref |
Expression |
1 |
|
funrel |
|- ( Fun A -> Rel A ) |
2 |
|
1st2nd |
|- ( ( Rel A /\ X e. A ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) |
3 |
1 2
|
sylan |
|- ( ( Fun A /\ X e. A ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) |
4 |
|
simpl1l |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> Fun A ) |
5 |
|
simpl3 |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> B C_ A ) |
6 |
|
simpr |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> ( 1st ` X ) e. dom B ) |
7 |
|
funssfv |
|- ( ( Fun A /\ B C_ A /\ ( 1st ` X ) e. dom B ) -> ( A ` ( 1st ` X ) ) = ( B ` ( 1st ` X ) ) ) |
8 |
4 5 6 7
|
syl3anc |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> ( A ` ( 1st ` X ) ) = ( B ` ( 1st ` X ) ) ) |
9 |
|
eleq1 |
|- ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( X e. A <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. A ) ) |
10 |
9
|
adantl |
|- ( ( Fun A /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) -> ( X e. A <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. A ) ) |
11 |
|
funopfv |
|- ( Fun A -> ( <. ( 1st ` X ) , ( 2nd ` X ) >. e. A -> ( A ` ( 1st ` X ) ) = ( 2nd ` X ) ) ) |
12 |
11
|
adantr |
|- ( ( Fun A /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) -> ( <. ( 1st ` X ) , ( 2nd ` X ) >. e. A -> ( A ` ( 1st ` X ) ) = ( 2nd ` X ) ) ) |
13 |
10 12
|
sylbid |
|- ( ( Fun A /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) -> ( X e. A -> ( A ` ( 1st ` X ) ) = ( 2nd ` X ) ) ) |
14 |
13
|
impancom |
|- ( ( Fun A /\ X e. A ) -> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( A ` ( 1st ` X ) ) = ( 2nd ` X ) ) ) |
15 |
14
|
imp |
|- ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) -> ( A ` ( 1st ` X ) ) = ( 2nd ` X ) ) |
16 |
15
|
3adant3 |
|- ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) -> ( A ` ( 1st ` X ) ) = ( 2nd ` X ) ) |
17 |
16
|
adantr |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> ( A ` ( 1st ` X ) ) = ( 2nd ` X ) ) |
18 |
8 17
|
eqtr3d |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> ( B ` ( 1st ` X ) ) = ( 2nd ` X ) ) |
19 |
|
funss |
|- ( B C_ A -> ( Fun A -> Fun B ) ) |
20 |
19
|
com12 |
|- ( Fun A -> ( B C_ A -> Fun B ) ) |
21 |
20
|
adantr |
|- ( ( Fun A /\ X e. A ) -> ( B C_ A -> Fun B ) ) |
22 |
21
|
imp |
|- ( ( ( Fun A /\ X e. A ) /\ B C_ A ) -> Fun B ) |
23 |
22
|
funfnd |
|- ( ( ( Fun A /\ X e. A ) /\ B C_ A ) -> B Fn dom B ) |
24 |
23
|
3adant2 |
|- ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) -> B Fn dom B ) |
25 |
|
fnopfvb |
|- ( ( B Fn dom B /\ ( 1st ` X ) e. dom B ) -> ( ( B ` ( 1st ` X ) ) = ( 2nd ` X ) <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. B ) ) |
26 |
24 25
|
sylan |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> ( ( B ` ( 1st ` X ) ) = ( 2nd ` X ) <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. B ) ) |
27 |
18 26
|
mpbid |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> <. ( 1st ` X ) , ( 2nd ` X ) >. e. B ) |
28 |
|
eleq1 |
|- ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( X e. B <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. B ) ) |
29 |
28
|
3ad2ant2 |
|- ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) -> ( X e. B <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. B ) ) |
30 |
29
|
adantr |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> ( X e. B <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. B ) ) |
31 |
27 30
|
mpbird |
|- ( ( ( ( Fun A /\ X e. A ) /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ B C_ A ) /\ ( 1st ` X ) e. dom B ) -> X e. B ) |
32 |
31
|
3exp1 |
|- ( ( Fun A /\ X e. A ) -> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( B C_ A -> ( ( 1st ` X ) e. dom B -> X e. B ) ) ) ) |
33 |
3 32
|
mpd |
|- ( ( Fun A /\ X e. A ) -> ( B C_ A -> ( ( 1st ` X ) e. dom B -> X e. B ) ) ) |
34 |
33
|
ex |
|- ( Fun A -> ( X e. A -> ( B C_ A -> ( ( 1st ` X ) e. dom B -> X e. B ) ) ) ) |
35 |
34
|
com23 |
|- ( Fun A -> ( B C_ A -> ( X e. A -> ( ( 1st ` X ) e. dom B -> X e. B ) ) ) ) |
36 |
35
|
3imp |
|- ( ( Fun A /\ B C_ A /\ X e. A ) -> ( ( 1st ` X ) e. dom B -> X e. B ) ) |