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 \land B \subseteq A \land X \in A) \to (1^{st} (X) \in dom B \to X \in B)$

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun A \to Rel A$
2		1st2nd	$⊢ (Rel A \land X \in A) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
3	1 2	sylan	$⊢ (Fun A \land X \in A) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
4		simpl1l	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to Fun A$
5		simpl3	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to B \subseteq A$
6		simpr	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to 1^{st} (X) \in dom B$
7		funssfv	$⊢ (Fun A \land B \subseteq A \land 1^{st} (X) \in dom B) \to A (1^{st} (X)) = B (1^{st} (X))$
8	4 5 6 7	syl3anc	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to A (1^{st} (X)) = B (1^{st} (X))$
9		eleq1	$⊢ X = ⟨1^{st} (X), 2^{nd} (X)⟩ \to (X \in A \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in A)$
10	9	adantl	$⊢ (Fun A \land X = ⟨1^{st} (X), 2^{nd} (X)⟩) \to (X \in A \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in A)$
11		funopfv	$⊢ Fun A \to (⟨1^{st} (X), 2^{nd} (X)⟩ \in A \to A (1^{st} (X)) = 2^{nd} (X))$
12	11	adantr	$⊢ (Fun A \land X = ⟨1^{st} (X), 2^{nd} (X)⟩) \to (⟨1^{st} (X), 2^{nd} (X)⟩ \in A \to A (1^{st} (X)) = 2^{nd} (X))$
13	10 12	sylbid	$⊢ (Fun A \land X = ⟨1^{st} (X), 2^{nd} (X)⟩) \to (X \in A \to A (1^{st} (X)) = 2^{nd} (X))$
14	13	impancom	$⊢ (Fun A \land X \in A) \to (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \to A (1^{st} (X)) = 2^{nd} (X))$
15	14	imp	$⊢ ((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩) \to A (1^{st} (X)) = 2^{nd} (X)$
16	15	3adant3	$⊢ ((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \to A (1^{st} (X)) = 2^{nd} (X)$
17	16	adantr	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to A (1^{st} (X)) = 2^{nd} (X)$
18	8 17	eqtr3d	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to B (1^{st} (X)) = 2^{nd} (X)$
19		funss	$⊢ B \subseteq A \to (Fun A \to Fun B)$
20	19	com12	$⊢ Fun A \to (B \subseteq A \to Fun B)$
21	20	adantr	$⊢ (Fun A \land X \in A) \to (B \subseteq A \to Fun B)$
22	21	imp	$⊢ ((Fun A \land X \in A) \land B \subseteq A) \to Fun B$
23	22	funfnd	$⊢ ((Fun A \land X \in A) \land B \subseteq A) \to B Fn dom B$
24	23	3adant2	$⊢ ((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \to B Fn dom B$
25		fnopfvb	$⊢ (B Fn dom B \land 1^{st} (X) \in dom B) \to (B (1^{st} (X)) = 2^{nd} (X) \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in B)$
26	24 25	sylan	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to (B (1^{st} (X)) = 2^{nd} (X) \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in B)$
27	18 26	mpbid	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to ⟨1^{st} (X), 2^{nd} (X)⟩ \in B$
28		eleq1	$⊢ X = ⟨1^{st} (X), 2^{nd} (X)⟩ \to (X \in B \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in B)$
29	28	3ad2ant2	$⊢ ((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \to (X \in B \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in B)$
30	29	adantr	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to (X \in B \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in B)$
31	27 30	mpbird	$⊢ (((Fun A \land X \in A) \land X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land B \subseteq A) \land 1^{st} (X) \in dom B) \to X \in B$
32	31	3exp1	$⊢ (Fun A \land X \in A) \to (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \to (B \subseteq A \to (1^{st} (X) \in dom B \to X \in B)))$
33	3 32	mpd	$⊢ (Fun A \land X \in A) \to (B \subseteq A \to (1^{st} (X) \in dom B \to X \in B))$
34	33	ex	$⊢ Fun A \to (X \in A \to (B \subseteq A \to (1^{st} (X) \in dom B \to X \in B)))$
35	34	com23	$⊢ Fun A \to (B \subseteq A \to (X \in A \to (1^{st} (X) \in dom B \to X \in B)))$
36	35	3imp	$⊢ (Fun A \land B \subseteq A \land X \in A) \to (1^{st} (X) \in dom B \to X \in B)$

Metamath Proof Explorer

Theorem funelss

Proof