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

Proof

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

Metamath Proof Explorer

Theorem funelss

Proof