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 𝐴𝐵𝐴𝑋𝐴 ) → ( ( 1st𝑋 ) ∈ dom 𝐵𝑋𝐵 ) )

Proof

Step Hyp Ref Expression
1 funrel ( Fun 𝐴 → Rel 𝐴 )
2 1st2nd ( ( Rel 𝐴𝑋𝐴 ) → 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ )
3 1 2 sylan ( ( Fun 𝐴𝑋𝐴 ) → 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ )
4 simpl1l ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → Fun 𝐴 )
5 simpl3 ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → 𝐵𝐴 )
6 simpr ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( 1st𝑋 ) ∈ dom 𝐵 )
7 funssfv ( ( Fun 𝐴𝐵𝐴 ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 𝐵 ‘ ( 1st𝑋 ) ) )
8 4 5 6 7 syl3anc ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 𝐵 ‘ ( 1st𝑋 ) ) )
9 eleq1 ( 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ → ( 𝑋𝐴 ↔ ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐴 ) )
10 9 adantl ( ( Fun 𝐴𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ) → ( 𝑋𝐴 ↔ ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐴 ) )
11 funopfv ( Fun 𝐴 → ( ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐴 → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) ) )
12 11 adantr ( ( Fun 𝐴𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ) → ( ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐴 → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) ) )
13 10 12 sylbid ( ( Fun 𝐴𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ) → ( 𝑋𝐴 → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) ) )
14 13 impancom ( ( Fun 𝐴𝑋𝐴 ) → ( 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) ) )
15 14 imp ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ) → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) )
16 15 3adant3 ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) )
17 16 adantr ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( 𝐴 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) )
18 8 17 eqtr3d ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( 𝐵 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) )
19 funss ( 𝐵𝐴 → ( Fun 𝐴 → Fun 𝐵 ) )
20 19 com12 ( Fun 𝐴 → ( 𝐵𝐴 → Fun 𝐵 ) )
21 20 adantr ( ( Fun 𝐴𝑋𝐴 ) → ( 𝐵𝐴 → Fun 𝐵 ) )
22 21 imp ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝐵𝐴 ) → Fun 𝐵 )
23 22 funfnd ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝐵𝐴 ) → 𝐵 Fn dom 𝐵 )
24 23 3adant2 ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) → 𝐵 Fn dom 𝐵 )
25 fnopfvb ( ( 𝐵 Fn dom 𝐵 ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( ( 𝐵 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) ↔ ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐵 ) )
26 24 25 sylan ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( ( 𝐵 ‘ ( 1st𝑋 ) ) = ( 2nd𝑋 ) ↔ ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐵 ) )
27 18 26 mpbid ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐵 )
28 eleq1 ( 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ → ( 𝑋𝐵 ↔ ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐵 ) )
29 28 3ad2ant2 ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) → ( 𝑋𝐵 ↔ ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐵 ) )
30 29 adantr ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → ( 𝑋𝐵 ↔ ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∈ 𝐵 ) )
31 27 30 mpbird ( ( ( ( Fun 𝐴𝑋𝐴 ) ∧ 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ ∧ 𝐵𝐴 ) ∧ ( 1st𝑋 ) ∈ dom 𝐵 ) → 𝑋𝐵 )
32 31 3exp1 ( ( Fun 𝐴𝑋𝐴 ) → ( 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ → ( 𝐵𝐴 → ( ( 1st𝑋 ) ∈ dom 𝐵𝑋𝐵 ) ) ) )
33 3 32 mpd ( ( Fun 𝐴𝑋𝐴 ) → ( 𝐵𝐴 → ( ( 1st𝑋 ) ∈ dom 𝐵𝑋𝐵 ) ) )
34 33 ex ( Fun 𝐴 → ( 𝑋𝐴 → ( 𝐵𝐴 → ( ( 1st𝑋 ) ∈ dom 𝐵𝑋𝐵 ) ) ) )
35 34 com23 ( Fun 𝐴 → ( 𝐵𝐴 → ( 𝑋𝐴 → ( ( 1st𝑋 ) ∈ dom 𝐵𝑋𝐵 ) ) ) )
36 35 3imp ( ( Fun 𝐴𝐵𝐴𝑋𝐴 ) → ( ( 1st𝑋 ) ∈ dom 𝐵𝑋𝐵 ) )