uniimaprimaeqfv

Description: The union of the image of the preimage of a function value is the function value. (Contributed by AV, 12-Mar-2024)

		Ref	Expression
	Assertion	uniimaprimaeqfv	$⊢ (F Fn A \land X \in A) \to ⋃ F [F^{-1} [\{F (X)\}]] = F (X)$

Step	Hyp	Ref	Expression
1		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
2	1	biimpi	$⊢ F Fn A \to F : A ⟶ ran F$
3	2	adantr	$⊢ (F Fn A \land X \in A) \to F : A ⟶ ran F$
4		cnvimass	$⊢ F^{-1} [\{F (X)\}] \subseteq dom F$
5		fndm	$⊢ F Fn A \to dom F = A$
6	4 5	sseqtrid	$⊢ F Fn A \to F^{-1} [\{F (X)\}] \subseteq A$
7	6	adantr	$⊢ (F Fn A \land X \in A) \to F^{-1} [\{F (X)\}] \subseteq A$
8		preimafvsnel	$⊢ (F Fn A \land X \in A) \to X \in F^{-1} [\{F (X)\}]$
9	3 7 8	3jca	$⊢ (F Fn A \land X \in A) \to (F : A ⟶ ran F \land F^{-1} [\{F (X)\}] \subseteq A \land X \in F^{-1} [\{F (X)\}])$
10		fniniseg	$⊢ F Fn A \to (x \in F^{-1} [\{F (X)\}] \leftrightarrow (x \in A \land F (x) = F (X)))$
11	10	adantr	$⊢ (F Fn A \land X \in A) \to (x \in F^{-1} [\{F (X)\}] \leftrightarrow (x \in A \land F (x) = F (X)))$
12		simpr	$⊢ (x \in A \land F (x) = F (X)) \to F (x) = F (X)$
13	11 12	syl6bi	$⊢ (F Fn A \land X \in A) \to (x \in F^{-1} [\{F (X)\}] \to F (x) = F (X))$
14	13	ralrimiv	$⊢ (F Fn A \land X \in A) \to \forall x \in F^{-1} [\{F (X)\}] F (x) = F (X)$
15		uniimafveqt	$⊢ (F : A ⟶ ran F \land F^{-1} [\{F (X)\}] \subseteq A \land X \in F^{-1} [\{F (X)\}]) \to (\forall x \in F^{-1} [\{F (X)\}] F (x) = F (X) \to ⋃ F [F^{-1} [\{F (X)\}]] = F (X))$
16	9 14 15	sylc	$⊢ (F Fn A \land X \in A) \to ⋃ F [F^{-1} [\{F (X)\}]] = F (X)$

Metamath Proof Explorer