Metamath Proof Explorer


Theorem funelss

Description: If the first component of an element of a function is in the domain of a subset of the function, the element is a member of this subset. (Contributed by AV, 27-Oct-2023)

Ref Expression
Assertion funelss
|- ( ( Fun A /\ B C_ A /\ X e. A ) -> ( ( 1st ` X ) e. dom B -> X e. B ) )

Proof

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