imasetpreimafvbijlemf1

Description: Lemma for imasetpreimafvbij : the mapping H is an injective function into the range of function F . (Contributed by AV, 9-Mar-2024) (Revised by AV, 22-Mar-2024)

	Ref	Expression
Hypotheses	fundcmpsurinj.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
	fundcmpsurinj.h	$⊢ H = (p \in P ⟼ ⋃ F [p])$
Assertion	imasetpreimafvbijlemf1	$⊢ F Fn A \to H : P \underset{1-1}{⟶} F [A]$

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2		fundcmpsurinj.h	$⊢ H = (p \in P ⟼ ⋃ F [p])$
3	1 2	imasetpreimafvbijlemf	$⊢ F Fn A \to H : P ⟶ F [A]$
4	1 2	imasetpreimafvbijlemfv1	$⊢ (F Fn A \land s \in P) \to \exists b \in s H (s) = F (b)$
5	1 2	imasetpreimafvbijlemfv1	$⊢ (F Fn A \land r \in P) \to \exists a \in r H (r) = F (a)$
6	4 5	anim12dan	$⊢ (F Fn A \land (s \in P \land r \in P)) \to (\exists b \in s H (s) = F (b) \land \exists a \in r H (r) = F (a))$
7		eqeq12	$⊢ (H (s) = F (b) \land H (r) = F (a)) \to (H (s) = H (r) \leftrightarrow F (b) = F (a))$
8	7	ancoms	$⊢ (H (r) = F (a) \land H (s) = F (b)) \to (H (s) = H (r) \leftrightarrow F (b) = F (a))$
9	8	adantl	$⊢ ((((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \land (H (r) = F (a) \land H (s) = F (b))) \to (H (s) = H (r) \leftrightarrow F (b) = F (a))$
10		simplll	$⊢ (((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \to F Fn A$
11		simpllr	$⊢ (((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \to (s \in P \land r \in P)$
12		simpr	$⊢ ((F Fn A \land (s \in P \land r \in P)) \land b \in s) \to b \in s$
13	12	anim1i	$⊢ (((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \to (b \in s \land a \in r)$
14	1	elsetpreimafveq	$⊢ (F Fn A \land (s \in P \land r \in P) \land (b \in s \land a \in r)) \to (F (b) = F (a) \to s = r)$
15	10 11 13 14	syl3anc	$⊢ (((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \to (F (b) = F (a) \to s = r)$
16	15	adantr	$⊢ ((((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \land (H (r) = F (a) \land H (s) = F (b))) \to (F (b) = F (a) \to s = r)$
17	9 16	sylbid	$⊢ ((((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \land (H (r) = F (a) \land H (s) = F (b))) \to (H (s) = H (r) \to s = r)$
18	17	exp32	$⊢ (((F Fn A \land (s \in P \land r \in P)) \land b \in s) \land a \in r) \to (H (r) = F (a) \to (H (s) = F (b) \to (H (s) = H (r) \to s = r)))$
19	18	rexlimdva	$⊢ ((F Fn A \land (s \in P \land r \in P)) \land b \in s) \to (\exists a \in r H (r) = F (a) \to (H (s) = F (b) \to (H (s) = H (r) \to s = r)))$
20	19	com23	$⊢ ((F Fn A \land (s \in P \land r \in P)) \land b \in s) \to (H (s) = F (b) \to (\exists a \in r H (r) = F (a) \to (H (s) = H (r) \to s = r)))$
21	20	rexlimdva	$⊢ (F Fn A \land (s \in P \land r \in P)) \to (\exists b \in s H (s) = F (b) \to (\exists a \in r H (r) = F (a) \to (H (s) = H (r) \to s = r)))$
22	21	impd	$⊢ (F Fn A \land (s \in P \land r \in P)) \to ((\exists b \in s H (s) = F (b) \land \exists a \in r H (r) = F (a)) \to (H (s) = H (r) \to s = r))$
23	6 22	mpd	$⊢ (F Fn A \land (s \in P \land r \in P)) \to (H (s) = H (r) \to s = r)$
24	23	ralrimivva	$⊢ F Fn A \to \forall s \in P \forall r \in P (H (s) = H (r) \to s = r)$
25		dff13	$⊢ H : P \underset{1-1}{⟶} F [A] \leftrightarrow (H : P ⟶ F [A] \land \forall s \in P \forall r \in P (H (s) = H (r) \to s = r))$
26	3 24 25	sylanbrc	$⊢ F Fn A \to H : P \underset{1-1}{⟶} F [A]$

Metamath Proof Explorer

Theorem imasetpreimafvbijlemf1

Proof