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