mpof1o2d

Description: Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by SN, 11-Mar-2025)

	Ref	Expression
Hypotheses	mpof1o2d.f	$⊢ F = (x \in A, y \in B ⟼ C)$
	mpof1o2d.r	$⊢ (φ \land (x \in A \land y \in B)) \to C \in D$
	mpof1o2d.i	$⊢ (φ \land z \in D) \to I \in A$
	mpof1o2d.j	$⊢ (φ \land z \in D) \to J \in B$
	mpof1o2d.1	$⊢ (φ \land ((x \in A \land y \in B) \land z \in D)) \to ((x = I \land y = J) \leftrightarrow z = C)$
Assertion	mpof1o2d	$⊢ φ \to F : A \times B \underset{1-1 onto}{⟶} D$

Proof

Step	Hyp	Ref	Expression
1		mpof1o2d.f	$⊢ F = (x \in A, y \in B ⟼ C)$
2		mpof1o2d.r	$⊢ (φ \land (x \in A \land y \in B)) \to C \in D$
3		mpof1o2d.i	$⊢ (φ \land z \in D) \to I \in A$
4		mpof1o2d.j	$⊢ (φ \land z \in D) \to J \in B$
5		mpof1o2d.1	$⊢ (φ \land ((x \in A \land y \in B) \land z \in D)) \to ((x = I \land y = J) \leftrightarrow z = C)$
6		mpompts	$⊢ (x \in A, y \in B ⟼ C) = (w \in (A \times B) ⟼ ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C)$
7	1 6	eqtri	$⊢ F = (w \in (A \times B) ⟼ ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C)$
8		xp1st	$⊢ w \in (A \times B) \to 1^{st} (w) \in A$
9		xp2nd	$⊢ w \in (A \times B) \to 2^{nd} (w) \in B$
10	2	anassrs	$⊢ ((φ \land x \in A) \land y \in B) \to C \in D$
11	10	ralrimiva	$⊢ (φ \land x \in A) \to \forall y \in B C \in D$
12		rspcsbela	$⊢ (2^{nd} (w) \in B \land \forall y \in B C \in D) \to ⦋ 2^{nd} (w) / y ⦌ C \in D$
13	9 11 12	syl2anr	$⊢ ((φ \land x \in A) \land w \in (A \times B)) \to ⦋ 2^{nd} (w) / y ⦌ C \in D$
14	13	an32s	$⊢ ((φ \land w \in (A \times B)) \land x \in A) \to ⦋ 2^{nd} (w) / y ⦌ C \in D$
15	14	ralrimiva	$⊢ (φ \land w \in (A \times B)) \to \forall x \in A ⦋ 2^{nd} (w) / y ⦌ C \in D$
16		rspcsbela	$⊢ (1^{st} (w) \in A \land \forall x \in A ⦋ 2^{nd} (w) / y ⦌ C \in D) \to ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C \in D$
17	8 15 16	syl2an2	$⊢ (φ \land w \in (A \times B)) \to ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C \in D$
18	3 4	opelxpd	$⊢ (φ \land z \in D) \to ⟨I, J⟩ \in (A \times B)$
19	9	ad2antrl	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to 2^{nd} (w) \in B$
20		sbceq2g	$⊢ 2^{nd} (w) \in B \to (\underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} z = C \leftrightarrow z = ⦋ 2^{nd} (w) / y ⦌ C)$
21	19 20	syl	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to (\underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} z = C \leftrightarrow z = ⦋ 2^{nd} (w) / y ⦌ C)$
22	21	sbcbidv	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to (\underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} z = C \leftrightarrow \underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} z = ⦋ 2^{nd} (w) / y ⦌ C)$
23	8	ad2antrl	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to 1^{st} (w) \in A$
24	19	adantr	$⊢ ((φ \land (w \in (A \times B) \land z \in D)) \land x = 1^{st} (w)) \to 2^{nd} (w) \in B$
25		eqop	$⊢ w \in (A \times B) \to (w = ⟨I, J⟩ \leftrightarrow (1^{st} (w) = I \land 2^{nd} (w) = J))$
26	25	ad2antrl	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to (w = ⟨I, J⟩ \leftrightarrow (1^{st} (w) = I \land 2^{nd} (w) = J))$
27		eqeq1	$⊢ x = 1^{st} (w) \to (x = I \leftrightarrow 1^{st} (w) = I)$
28		eqeq1	$⊢ y = 2^{nd} (w) \to (y = J \leftrightarrow 2^{nd} (w) = J)$
29	27 28	bi2anan9	$⊢ (x = 1^{st} (w) \land y = 2^{nd} (w)) \to ((x = I \land y = J) \leftrightarrow (1^{st} (w) = I \land 2^{nd} (w) = J))$
30	29	bicomd	$⊢ (x = 1^{st} (w) \land y = 2^{nd} (w)) \to ((1^{st} (w) = I \land 2^{nd} (w) = J) \leftrightarrow (x = I \land y = J))$
31	26 30	sylan9bb	$⊢ ((φ \land (w \in (A \times B) \land z \in D)) \land (x = 1^{st} (w) \land y = 2^{nd} (w))) \to (w = ⟨I, J⟩ \leftrightarrow (x = I \land y = J))$
32	31	anassrs	$⊢ (((φ \land (w \in (A \times B) \land z \in D)) \land x = 1^{st} (w)) \land y = 2^{nd} (w)) \to (w = ⟨I, J⟩ \leftrightarrow (x = I \land y = J))$
33		eleq1	$⊢ x = 1^{st} (w) \to (x \in A \leftrightarrow 1^{st} (w) \in A)$
34	8 33	syl5ibrcom	$⊢ w \in (A \times B) \to (x = 1^{st} (w) \to x \in A)$
35	34	imp	$⊢ (w \in (A \times B) \land x = 1^{st} (w)) \to x \in A$
36		eleq1	$⊢ y = 2^{nd} (w) \to (y \in B \leftrightarrow 2^{nd} (w) \in B)$
37	9 36	syl5ibrcom	$⊢ w \in (A \times B) \to (y = 2^{nd} (w) \to y \in B)$
38	37	imp	$⊢ (w \in (A \times B) \land y = 2^{nd} (w)) \to y \in B$
39	35 38	anim12dan	$⊢ (w \in (A \times B) \land (x = 1^{st} (w) \land y = 2^{nd} (w))) \to (x \in A \land y \in B)$
40	39	3impb	$⊢ (w \in (A \times B) \land x = 1^{st} (w) \land y = 2^{nd} (w)) \to (x \in A \land y \in B)$
41	40	3adant1r	$⊢ ((w \in (A \times B) \land z \in D) \land x = 1^{st} (w) \land y = 2^{nd} (w)) \to (x \in A \land y \in B)$
42		simp1r	$⊢ ((w \in (A \times B) \land z \in D) \land x = 1^{st} (w) \land y = 2^{nd} (w)) \to z \in D$
43	41 42	jca	$⊢ ((w \in (A \times B) \land z \in D) \land x = 1^{st} (w) \land y = 2^{nd} (w)) \to ((x \in A \land y \in B) \land z \in D)$
44	43 5	sylan2	$⊢ (φ \land ((w \in (A \times B) \land z \in D) \land x = 1^{st} (w) \land y = 2^{nd} (w))) \to ((x = I \land y = J) \leftrightarrow z = C)$
45	44	3anassrs	$⊢ (((φ \land (w \in (A \times B) \land z \in D)) \land x = 1^{st} (w)) \land y = 2^{nd} (w)) \to ((x = I \land y = J) \leftrightarrow z = C)$
46	32 45	bitr2d	$⊢ (((φ \land (w \in (A \times B) \land z \in D)) \land x = 1^{st} (w)) \land y = 2^{nd} (w)) \to (z = C \leftrightarrow w = ⟨I, J⟩)$
47	24 46	sbcied	$⊢ ((φ \land (w \in (A \times B) \land z \in D)) \land x = 1^{st} (w)) \to (\underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} z = C \leftrightarrow w = ⟨I, J⟩)$
48	23 47	sbcied	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to (\underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} z = C \leftrightarrow w = ⟨I, J⟩)$
49		sbceq2g	$⊢ 1^{st} (w) \in A \to (\underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} z = ⦋ 2^{nd} (w) / y ⦌ C \leftrightarrow z = ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C)$
50	23 49	syl	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to (\underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} z = ⦋ 2^{nd} (w) / y ⦌ C \leftrightarrow z = ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C)$
51	22 48 50	3bitr3d	$⊢ (φ \land (w \in (A \times B) \land z \in D)) \to (w = ⟨I, J⟩ \leftrightarrow z = ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C)$
52	7 17 18 51	f1o2d	$⊢ φ \to F : A \times B \underset{1-1 onto}{⟶} D$

Metamath Proof Explorer

Theorem mpof1o2d

Proof