2elresin

Description: Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994)

		Ref	Expression
	Assertion	2elresin	$⊢ (F Fn A \land G Fn B) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \leftrightarrow (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)})))$

Proof

Step	Hyp	Ref	Expression
1		fnop	$⊢ (F Fn A \land ⟨x, y⟩ \in F) \to x \in A$
2		fnop	$⊢ (G Fn B \land ⟨x, z⟩ \in G) \to x \in B$
3	1 2	anim12i	$⊢ ((F Fn A \land ⟨x, y⟩ \in F) \land (G Fn B \land ⟨x, z⟩ \in G)) \to (x \in A \land x \in B)$
4	3	an4s	$⊢ ((F Fn A \land G Fn B) \land (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \to (x \in A \land x \in B)$
5		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
6	4 5	sylibr	$⊢ ((F Fn A \land G Fn B) \land (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \to x \in (A \cap B)$
7		vex	$⊢ y \in V$
8	7	opres	$⊢ x \in (A \cap B) \to (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \leftrightarrow ⟨x, y⟩ \in F)$
9		vex	$⊢ z \in V$
10	9	opres	$⊢ x \in (A \cap B) \to (⟨x, z⟩ \in ({G ↾}_{(A \cap B)}) \leftrightarrow ⟨x, z⟩ \in G)$
11	8 10	anbi12d	$⊢ x \in (A \cap B) \to ((⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)})) \leftrightarrow (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G))$
12	11	biimprd	$⊢ x \in (A \cap B) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \to (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)})))$
13	6 12	syl	$⊢ ((F Fn A \land G Fn B) \land (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \to (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)})))$
14	13	ex	$⊢ (F Fn A \land G Fn B) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \to (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)}))))$
15	14	pm2.43d	$⊢ (F Fn A \land G Fn B) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \to (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)})))$
16		resss	$⊢ {F ↾}_{(A \cap B)} \subseteq F$
17	16	sseli	$⊢ ⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \to ⟨x, y⟩ \in F$
18		resss	$⊢ {G ↾}_{(A \cap B)} \subseteq G$
19	18	sseli	$⊢ ⟨x, z⟩ \in ({G ↾}_{(A \cap B)}) \to ⟨x, z⟩ \in G$
20	17 19	anim12i	$⊢ (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)})) \to (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)$
21	15 20	impbid1	$⊢ (F Fn A \land G Fn B) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \leftrightarrow (⟨x, y⟩ \in ({F ↾}_{(A \cap B)}) \land ⟨x, z⟩ \in ({G ↾}_{(A \cap B)})))$

Metamath Proof Explorer

Theorem 2elresin

Proof