f1od2

Description: Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by Thierry Arnoux, 17-Aug-2017)

	Ref	Expression
Hypotheses	f1od2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	f1od2.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑊 )
	f1od2.3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌 ) )
	f1od2.4	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ) )
Assertion	f1od2	⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		f1od2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		f1od2.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑊 )
3		f1od2.3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌 ) )
4		f1od2.4	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ) )
5	2	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑊 )
6	1	fnmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑊 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
7	5 6	syl	⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
8		opelxpi	⊢ ( ( 𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌 ) → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑋 × 𝑌 ) )
9	3 8	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑋 × 𝑌 ) )
10	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐷 ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑋 × 𝑌 ) )
11		eqid	⊢ ( 𝑧 ∈ 𝐷 ↦ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝑧 ∈ 𝐷 ↦ ⟨ 𝐼 , 𝐽 ⟩ )
12	11	fnmpt	⊢ ( ∀ 𝑧 ∈ 𝐷 ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( 𝑧 ∈ 𝐷 ↦ ⟨ 𝐼 , 𝐽 ⟩ ) Fn 𝐷 )
13	10 12	syl	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐷 ↦ ⟨ 𝐼 , 𝐽 ⟩ ) Fn 𝐷 )
14		elxp7	⊢ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ) )
15	14	anbi1i	⊢ ( ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( ( 𝑎 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
16		anass	⊢ ( ( ( 𝑎 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( 𝑎 ∈ ( V × V ) ∧ ( ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ) )
17	4	sbcbidv	⊢ ( 𝜑 → ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ) )
18	17	sbcbidv	⊢ ( 𝜑 → ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ) )
19		sbcan	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 = 𝐶 ) )
20		sbcan	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 ∈ 𝐴 ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 ∈ 𝐵 ) )
21		fvex	⊢ ( 2^nd ‘ 𝑎 ) ∈ V
22		sbcg	⊢ ( ( 2^nd ‘ 𝑎 ) ∈ V → ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
23	21 22	ax-mp	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 )
24		sbcel1v	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 ∈ 𝐵 ↔ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 )
25	23 24	anbi12i	⊢ ( ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 ∈ 𝐴 ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) )
26	20 25	bitri	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) )
27		sbceq2g	⊢ ( ( 2^nd ‘ 𝑎 ) ∈ V → ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 = 𝐶 ↔ 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
28	21 27	ax-mp	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 = 𝐶 ↔ 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 )
29	26 28	anbi12i	⊢ ( ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
30	19 29	bitri	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
31	30	sbcbii	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
32		sbcan	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
33		sbcan	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ↔ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) )
34		sbcel1v	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 ∈ 𝐴 ↔ ( 1^st ‘ 𝑎 ) ∈ 𝐴 )
35		fvex	⊢ ( 1^st ‘ 𝑎 ) ∈ V
36		sbcg	⊢ ( ( 1^st ‘ 𝑎 ) ∈ V → ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ↔ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) )
37	35 36	ax-mp	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ↔ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 )
38	34 37	anbi12i	⊢ ( ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ↔ ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) )
39	33 38	bitri	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ↔ ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) )
40		sbceq2g	⊢ ( ( 1^st ‘ 𝑎 ) ∈ V → ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ↔ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
41	35 40	ax-mp	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ↔ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 )
42	39 41	anbi12i	⊢ ( ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
43	31 32 42	3bitri	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) )
44		sbcan	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ↔ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 ∈ 𝐷 ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) )
45		sbcg	⊢ ( ( 2^nd ‘ 𝑎 ) ∈ V → ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷 ) )
46	21 45	ax-mp	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷 )
47		sbcan	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ↔ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 = 𝐼 ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 = 𝐽 ) )
48		sbcg	⊢ ( ( 2^nd ‘ 𝑎 ) ∈ V → ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 = 𝐼 ↔ 𝑥 = 𝐼 ) )
49	21 48	ax-mp	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 = 𝐼 ↔ 𝑥 = 𝐼 )
50		sbceq1g	⊢ ( ( 2^nd ‘ 𝑎 ) ∈ V → ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 = 𝐽 ↔ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝑦 = 𝐽 ) )
51	21 50	ax-mp	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 = 𝐽 ↔ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝑦 = 𝐽 )
52	21	csbvargi	⊢ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝑦 = ( 2^nd ‘ 𝑎 )
53	52	eqeq1i	⊢ ( ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝑦 = 𝐽 ↔ ( 2^nd ‘ 𝑎 ) = 𝐽 )
54	51 53	bitri	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 = 𝐽 ↔ ( 2^nd ‘ 𝑎 ) = 𝐽 )
55	49 54	anbi12i	⊢ ( ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑥 = 𝐼 ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑦 = 𝐽 ) ↔ ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) )
56	47 55	bitri	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ↔ ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) )
57	46 56	anbi12i	⊢ ( ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] 𝑧 ∈ 𝐷 ∧ [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) )
58	44 57	bitri	⊢ ( [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) )
59	58	sbcbii	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ↔ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) )
60		sbcan	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ↔ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 ∈ 𝐷 ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) )
61		sbcg	⊢ ( ( 1^st ‘ 𝑎 ) ∈ V → ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷 ) )
62	35 61	ax-mp	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷 )
63		sbcan	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ↔ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 = 𝐼 ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) = 𝐽 ) )
64		sbceq1g	⊢ ( ( 1^st ‘ 𝑎 ) ∈ V → ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 = 𝐼 ↔ ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ 𝑥 = 𝐼 ) )
65	35 64	ax-mp	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 = 𝐼 ↔ ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ 𝑥 = 𝐼 )
66	35	csbvargi	⊢ ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ 𝑥 = ( 1^st ‘ 𝑎 )
67	66	eqeq1i	⊢ ( ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ 𝑥 = 𝐼 ↔ ( 1^st ‘ 𝑎 ) = 𝐼 )
68	65 67	bitri	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 = 𝐼 ↔ ( 1^st ‘ 𝑎 ) = 𝐼 )
69		sbcg	⊢ ( ( 1^st ‘ 𝑎 ) ∈ V → ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) = 𝐽 ↔ ( 2^nd ‘ 𝑎 ) = 𝐽 ) )
70	35 69	ax-mp	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) = 𝐽 ↔ ( 2^nd ‘ 𝑎 ) = 𝐽 )
71	68 70	anbi12i	⊢ ( ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑥 = 𝐼 ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 2^nd ‘ 𝑎 ) = 𝐽 ) ↔ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) )
72	63 71	bitri	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ↔ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) )
73	62 72	anbi12i	⊢ ( ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] 𝑧 ∈ 𝐷 ∧ [ ( 1^st ‘ 𝑎 ) / 𝑥 ] ( 𝑥 = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) )
74	59 60 73	3bitri	⊢ ( [ ( 1^st ‘ 𝑎 ) / 𝑥 ] [ ( 2^nd ‘ 𝑎 ) / 𝑦 ] ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) )
75	18 43 74	3bitr3g	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ) )
76	75	anbi2d	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( V × V ) ∧ ( ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ) ↔ ( 𝑎 ∈ ( V × V ) ∧ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ) ) )
77	16 76	bitrid	⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( 𝑎 ∈ ( V × V ) ∧ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ) ) )
78		xpss	⊢ ( 𝑋 × 𝑌 ) ⊆ ( V × V )
79		simprr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) → 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ )
80	9	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( 𝑋 × 𝑌 ) )
81	79 80	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) → 𝑎 ∈ ( 𝑋 × 𝑌 ) )
82	78 81	sselid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) → 𝑎 ∈ ( V × V ) )
83	82	ex	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) → 𝑎 ∈ ( V × V ) ) )
84	83	pm4.71rd	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ↔ ( 𝑎 ∈ ( V × V ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) ) )
85		eqop	⊢ ( 𝑎 ∈ ( V × V ) → ( 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ↔ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) )
86	85	anbi2d	⊢ ( 𝑎 ∈ ( V × V ) → ( ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ↔ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ) )
87	86	pm5.32i	⊢ ( ( 𝑎 ∈ ( V × V ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) ↔ ( 𝑎 ∈ ( V × V ) ∧ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ) )
88	84 87	bitr2di	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( V × V ) ∧ ( 𝑧 ∈ 𝐷 ∧ ( ( 1^st ‘ 𝑎 ) = 𝐼 ∧ ( 2^nd ‘ 𝑎 ) = 𝐽 ) ) ) ↔ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) )
89	77 88	bitrd	⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑎 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝐵 ) ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) )
90	15 89	bitrid	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) ) )
91	90	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) } )
92		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
93	1 92	eqtri	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
94	93	cnveqi	⊢ ^◡ 𝐹 = ^◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
95		nfv	⊢ Ⅎ 𝑖 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 )
96		nfv	⊢ Ⅎ 𝑗 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 )
97		nfv	⊢ Ⅎ 𝑥 ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 )
98		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶
99	98	nfeq2	⊢ Ⅎ 𝑥 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶
100	97 99	nfan	⊢ Ⅎ 𝑥 ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 )
101		nfv	⊢ Ⅎ 𝑦 ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 )
102		nfcv	⊢ Ⅎ 𝑦 𝑖
103		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑗 / 𝑦 ⦌ 𝐶
104	102 103	nfcsbw	⊢ Ⅎ 𝑦 ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶
105	104	nfeq2	⊢ Ⅎ 𝑦 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶
106	101 105	nfan	⊢ Ⅎ 𝑦 ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 )
107		simpl	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → 𝑥 = 𝑖 )
108	107	eleq1d	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) )
109		simpr	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → 𝑦 = 𝑗 )
110	109	eleq1d	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑗 ∈ 𝐵 ) )
111	108 110	anbi12d	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) )
112		csbeq1a	⊢ ( 𝑦 = 𝑗 → 𝐶 = ⦋ 𝑗 / 𝑦 ⦌ 𝐶 )
113		csbeq1a	⊢ ( 𝑥 = 𝑖 → ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 )
114	112 113	sylan9eqr	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → 𝐶 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 )
115	114	eqeq2d	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑧 = 𝐶 ↔ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 ) )
116	111 115	anbi12d	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 ) ) )
117	95 96 100 106 116	cbvoprab12	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { ⟨ ⟨ 𝑖 , 𝑗 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 ) }
118	117	cnveqi	⊢ ^◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = ^◡ { ⟨ ⟨ 𝑖 , 𝑗 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 ) }
119		eleq1	⊢ ( 𝑎 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
120		opelxp	⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) )
121	119 120	bitrdi	⊢ ( 𝑎 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) )
122		csbcom	⊢ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶
123		csbcow	⊢ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶
124	123	csbeq2i	⊢ ⦋ 𝑖 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶
125	122 124	eqtri	⊢ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶
126	125	csbeq2i	⊢ ⦋ ( 1^st ‘ 𝑎 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑖 ⦌ ⦋ 𝑖 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶
127		csbcow	⊢ ⦋ ( 1^st ‘ 𝑎 ) / 𝑖 ⦌ ⦋ 𝑖 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶
128	126 127	eqtri	⊢ ⦋ ( 1^st ‘ 𝑎 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶
129		csbopeq1a	⊢ ( 𝑎 = ⟨ 𝑖 , 𝑗 ⟩ → ⦋ ( 1^st ‘ 𝑎 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑗 ⦌ ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 )
130	128 129	eqtr3id	⊢ ( 𝑎 = ⟨ 𝑖 , 𝑗 ⟩ → ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 )
131	130	eqeq2d	⊢ ( 𝑎 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ↔ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 ) )
132	121 131	anbi12d	⊢ ( 𝑎 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 ) ) )
133		xpss	⊢ ( 𝐴 × 𝐵 ) ⊆ ( V × V )
134	133	sseli	⊢ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) → 𝑎 ∈ ( V × V ) )
135	134	adantr	⊢ ( ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) → 𝑎 ∈ ( V × V ) )
136	132 135	cnvoprab	⊢ ^◡ { ⟨ ⟨ 𝑖 , 𝑗 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑧 = ⦋ 𝑖 / 𝑥 ⦌ ⦋ 𝑗 / 𝑦 ⦌ 𝐶 ) } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) }
137	94 118 136	3eqtri	⊢ ^◡ 𝐹 = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 = ⦋ ( 1^st ‘ 𝑎 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑎 ) / 𝑦 ⦌ 𝐶 ) }
138		df-mpt	⊢ ( 𝑧 ∈ 𝐷 ↦ ⟨ 𝐼 , 𝐽 ⟩ ) = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨ 𝐼 , 𝐽 ⟩ ) }
139	91 137 138	3eqtr4g	⊢ ( 𝜑 → ^◡ 𝐹 = ( 𝑧 ∈ 𝐷 ↦ ⟨ 𝐼 , 𝐽 ⟩ ) )
140	139	fneq1d	⊢ ( 𝜑 → ( ^◡ 𝐹 Fn 𝐷 ↔ ( 𝑧 ∈ 𝐷 ↦ ⟨ 𝐼 , 𝐽 ⟩ ) Fn 𝐷 ) )
141	13 140	mpbird	⊢ ( 𝜑 → ^◡ 𝐹 Fn 𝐷 )
142		dff1o4	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ 𝐷 ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ^◡ 𝐹 Fn 𝐷 ) )
143	7 141 142	sylanbrc	⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ 𝐷 )

Metamath Proof Explorer

Theorem f1od2

Proof