imarnf1pr

Description: The image of the range of a function F under a function E if F is a function from a pair into the domain of E . (Contributed by Alexander van der Vekens, 2-Feb-2018)

		Ref	Expression
	Assertion	imarnf1pr	$⊢ (X \in V \land Y \in W) \to (((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B)) \to E [ran F] = \{A, B\})$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ E : dom E ⟶ R \to E Fn dom E$
2	1	adantl	$⊢ (F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \to E Fn dom E$
3	2	adantr	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (X \in V \land Y \in W)) \to E Fn dom E$
4		simpll	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (X \in V \land Y \in W)) \to F : \{X, Y\} ⟶ dom E$
5		prid1g	$⊢ X \in V \to X \in \{X, Y\}$
6	5	adantr	$⊢ (X \in V \land Y \in W) \to X \in \{X, Y\}$
7	6	adantl	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (X \in V \land Y \in W)) \to X \in \{X, Y\}$
8	4 7	ffvelcdmd	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (X \in V \land Y \in W)) \to F (X) \in dom E$
9		prid2g	$⊢ Y \in W \to Y \in \{X, Y\}$
10	9	ad2antll	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (X \in V \land Y \in W)) \to Y \in \{X, Y\}$
11	4 10	ffvelcdmd	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (X \in V \land Y \in W)) \to F (Y) \in dom E$
12		fnimapr	$⊢ (E Fn dom E \land F (X) \in dom E \land F (Y) \in dom E) \to E [\{F (X), F (Y)\}] = \{E (F (X)), E (F (Y))\}$
13	3 8 11 12	syl3anc	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (X \in V \land Y \in W)) \to E [\{F (X), F (Y)\}] = \{E (F (X)), E (F (Y))\}$
14	13	ex	$⊢ (F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \to ((X \in V \land Y \in W) \to E [\{F (X), F (Y)\}] = \{E (F (X)), E (F (Y))\})$
15	14	adantr	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B)) \to ((X \in V \land Y \in W) \to E [\{F (X), F (Y)\}] = \{E (F (X)), E (F (Y))\})$
16	15	impcom	$⊢ ((X \in V \land Y \in W) \land ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B))) \to E [\{F (X), F (Y)\}] = \{E (F (X)), E (F (Y))\}$
17		ffn	$⊢ F : \{X, Y\} ⟶ dom E \to F Fn \{X, Y\}$
18		rnfdmpr	$⊢ (X \in V \land Y \in W) \to (F Fn \{X, Y\} \to ran F = \{F (X), F (Y)\})$
19	17 18	syl5com	$⊢ F : \{X, Y\} ⟶ dom E \to ((X \in V \land Y \in W) \to ran F = \{F (X), F (Y)\})$
20	19	adantr	$⊢ (F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \to ((X \in V \land Y \in W) \to ran F = \{F (X), F (Y)\})$
21	20	adantr	$⊢ ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B)) \to ((X \in V \land Y \in W) \to ran F = \{F (X), F (Y)\})$
22	21	impcom	$⊢ ((X \in V \land Y \in W) \land ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B))) \to ran F = \{F (X), F (Y)\}$
23	22	eqcomd	$⊢ ((X \in V \land Y \in W) \land ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B))) \to \{F (X), F (Y)\} = ran F$
24	23	imaeq2d	$⊢ ((X \in V \land Y \in W) \land ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B))) \to E [\{F (X), F (Y)\}] = E [ran F]$
25		preq12	$⊢ (E (F (X)) = A \land E (F (Y)) = B) \to \{E (F (X)), E (F (Y))\} = \{A, B\}$
26	25	ad2antll	$⊢ ((X \in V \land Y \in W) \land ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B))) \to \{E (F (X)), E (F (Y))\} = \{A, B\}$
27	16 24 26	3eqtr3d	$⊢ ((X \in V \land Y \in W) \land ((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B))) \to E [ran F] = \{A, B\}$
28	27	ex	$⊢ (X \in V \land Y \in W) \to (((F : \{X, Y\} ⟶ dom E \land E : dom E ⟶ R) \land (E (F (X)) = A \land E (F (Y)) = B)) \to E [ran F] = \{A, B\})$

Metamath Proof Explorer

Theorem imarnf1pr

Proof