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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	mpof1o2d.r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
	mpof1o2d.i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝐼 ∈ 𝐴 )
	mpof1o2d.j	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝐽 ∈ 𝐵 )
	mpof1o2d.1	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ↔ 𝑧 = 𝐶 ) )
Assertion	mpof1o2d	⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		mpof1o2d.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		mpof1o2d.r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
3		mpof1o2d.i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝐼 ∈ 𝐴 )
4		mpof1o2d.j	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝐽 ∈ 𝐵 )
5		mpof1o2d.1	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ↔ 𝑧 = 𝐶 ) )
6		mpompts	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 )
7	1 6	eqtri	⊢ 𝐹 = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 )
8		xp1st	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 1^st ‘ 𝑤 ) ∈ 𝐴 )
9		xp2nd	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 2^nd ‘ 𝑤 ) ∈ 𝐵 )
10	2	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 )
11	10	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 )
12		rspcsbela	⊢ ( ( ( 2^nd ‘ 𝑤 ) ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ) → ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
13	9 11 12	syl2anr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) → ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
14	13	an32s	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
15	14	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
16		rspcsbela	⊢ ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) → ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
17	8 15 16	syl2an2	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) → ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
18	3 4	opelxpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝐴 × 𝐵 ) )
19	9	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( 2^nd ‘ 𝑤 ) ∈ 𝐵 )
20		sbceq2g	⊢ ( ( 2^nd ‘ 𝑤 ) ∈ 𝐵 → ( [ ( 2^nd ‘ 𝑤 ) / 𝑦 ] 𝑧 = 𝐶 ↔ 𝑧 = ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) )
21	19 20	syl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( [ ( 2^nd ‘ 𝑤 ) / 𝑦 ] 𝑧 = 𝐶 ↔ 𝑧 = ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) )
22	21	sbcbidv	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( [ ( 1^st ‘ 𝑤 ) / 𝑥 ] [ ( 2^nd ‘ 𝑤 ) / 𝑦 ] 𝑧 = 𝐶 ↔ [ ( 1^st ‘ 𝑤 ) / 𝑥 ] 𝑧 = ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) )
23	8	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( 1^st ‘ 𝑤 ) ∈ 𝐴 )
24	19	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ) → ( 2^nd ‘ 𝑤 ) ∈ 𝐵 )
25		eqop	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ↔ ( ( 1^st ‘ 𝑤 ) = 𝐼 ∧ ( 2^nd ‘ 𝑤 ) = 𝐽 ) ) )
26	25	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ↔ ( ( 1^st ‘ 𝑤 ) = 𝐼 ∧ ( 2^nd ‘ 𝑤 ) = 𝐽 ) ) )
27		eqeq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑤 ) → ( 𝑥 = 𝐼 ↔ ( 1^st ‘ 𝑤 ) = 𝐼 ) )
28		eqeq1	⊢ ( 𝑦 = ( 2^nd ‘ 𝑤 ) → ( 𝑦 = 𝐽 ↔ ( 2^nd ‘ 𝑤 ) = 𝐽 ) )
29	27 28	bi2anan9	⊢ ( ( 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ↔ ( ( 1^st ‘ 𝑤 ) = 𝐼 ∧ ( 2^nd ‘ 𝑤 ) = 𝐽 ) ) )
30	29	bicomd	⊢ ( ( 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( ( ( 1^st ‘ 𝑤 ) = 𝐼 ∧ ( 2^nd ‘ 𝑤 ) = 𝐽 ) ↔ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) )
31	26 30	sylan9bb	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) ∧ ( 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) ) → ( 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ↔ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) )
32	31	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ↔ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) )
33		eleq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑤 ) → ( 𝑥 ∈ 𝐴 ↔ ( 1^st ‘ 𝑤 ) ∈ 𝐴 ) )
34	8 33	syl5ibrcom	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 𝑥 = ( 1^st ‘ 𝑤 ) → 𝑥 ∈ 𝐴 ) )
35	34	imp	⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ) → 𝑥 ∈ 𝐴 )
36		eleq1	⊢ ( 𝑦 = ( 2^nd ‘ 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ ( 2^nd ‘ 𝑤 ) ∈ 𝐵 ) )
37	9 36	syl5ibrcom	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → ( 𝑦 = ( 2^nd ‘ 𝑤 ) → 𝑦 ∈ 𝐵 ) )
38	37	imp	⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → 𝑦 ∈ 𝐵 )
39	35 38	anim12dan	⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
40	39	3impb	⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
41	40	3adant1r	⊢ ( ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
42		simp1r	⊢ ( ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → 𝑧 ∈ 𝐷 )
43	41 42	jca	⊢ ( ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) )
44	43 5	sylan2	⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) ) → ( ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ↔ 𝑧 = 𝐶 ) )
45	44	3anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ↔ 𝑧 = 𝐶 ) )
46	32 45	bitr2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ) ∧ 𝑦 = ( 2^nd ‘ 𝑤 ) ) → ( 𝑧 = 𝐶 ↔ 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ) )
47	24 46	sbcied	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) ∧ 𝑥 = ( 1^st ‘ 𝑤 ) ) → ( [ ( 2^nd ‘ 𝑤 ) / 𝑦 ] 𝑧 = 𝐶 ↔ 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ) )
48	23 47	sbcied	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( [ ( 1^st ‘ 𝑤 ) / 𝑥 ] [ ( 2^nd ‘ 𝑤 ) / 𝑦 ] 𝑧 = 𝐶 ↔ 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ) )
49		sbceq2g	⊢ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 → ( [ ( 1^st ‘ 𝑤 ) / 𝑥 ] 𝑧 = ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ↔ 𝑧 = ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) )
50	23 49	syl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( [ ( 1^st ‘ 𝑤 ) / 𝑥 ] 𝑧 = ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ↔ 𝑧 = ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) )
51	22 48 50	3bitr3d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐷 ) ) → ( 𝑤 = ⟨ 𝐼 , 𝐽 ⟩ ↔ 𝑧 = ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) )
52	7 17 18 51	f1o2d	⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ 𝐷 )

Metamath Proof Explorer

Theorem mpof1o2d

Proof