Theorem 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	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
	f1od2.2	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to C\in W$$
	f1od2.3	$$⊢\left(\phi \wedge z\in D\right)\to \left(I\in X\wedge J\in Y\right)$$
	f1od2.4	$$⊢\phi \to \left(\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\right)$$
Assertion	f1od2	$$⊢\phi \to F:A\times B\underset{1-1\; onto}{⟶}D$$

Proof

Step	Hyp	Ref	Expression
1		f1od2.1	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
2		f1od2.2	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to C\in W$$
3		f1od2.3	$$⊢\left(\phi \wedge z\in D\right)\to \left(I\in X\wedge J\in Y\right)$$
4		f1od2.4	$$⊢\phi \to \left(\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\right)$$
5	2	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in BC\in W$$
6	1	fnmpo	$$⊢\forall x\in A\forall y\in BC\in W\to FFn\left(A\times B\right)$$
7	5 6	syl	$$⊢\phi \to FFn\left(A\times B\right)$$
8		opelxpi	$$⊢\left(I\in X\wedge J\in Y\right)\to ⟨I,J⟩\in \left(X\times Y\right)$$
9	3 8	syl	$$⊢\left(\phi \wedge z\in D\right)\to ⟨I,J⟩\in \left(X\times Y\right)$$
10	9	ralrimiva	$$⊢\phi \to \forall z\in D⟨I,J⟩\in \left(X\times Y\right)$$
11		eqid	$$⊢\left(z\in D⟼⟨I,J⟩\right)=\left(z\in D⟼⟨I,J⟩\right)$$
12	11	fnmpt	$$⊢\forall z\in D⟨I,J⟩\in \left(X\times Y\right)\to \left(z\in D⟼⟨I,J⟩\right)FnD$$
13	10 12	syl	$$⊢\phi \to \left(z\in D⟼⟨I,J⟩\right)FnD$$
14		elxp7	$$⊢a\in \left(A\times B\right)\leftrightarrow \left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\right)$$
15	14	anbi1i	$$⊢\left(a\in \left(A\times B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(\left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)$$
16		anass	$$⊢\left(\left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(\left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\right)$$
17	4	sbcbidv	$$⊢\phi \to \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\right)$$
18	17	sbcbidv	$$⊢\phi \to \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\right)$$
19		sbcan	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x\in A\wedge y\in B\right)\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z=C\right)$$
20		sbcan	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x\in A\wedge y\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y\in B\right)$$
21		fvex	$$⊢2^{nd}\left(a\right)\in \mathrm{V}$$
22		sbcg	$$⊢2^{nd}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x\in A\leftrightarrow x\in A\right)$$
23	21 22	ax-mp	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x\in A\leftrightarrow x\in A$$
24		sbcel1v	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y\in B\leftrightarrow 2^{nd}\left(a\right)\in B$$
25	23 24	anbi12i	$$⊢\left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y\in B\right)\leftrightarrow \left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)$$
26	20 25	bitri	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x\in A\wedge y\in B\right)\leftrightarrow \left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)$$
27		sbceq2g	$$⊢2^{nd}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z=C\leftrightarrow z=⦋2^{nd}\left(a\right)/y⦌C\right)$$
28	21 27	ax-mp	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z=C\leftrightarrow z=⦋2^{nd}\left(a\right)/y⦌C$$
29	26 28	anbi12i	$$⊢\left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x\in A\wedge y\in B\right)\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z=C\right)\leftrightarrow \left(\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋2^{nd}\left(a\right)/y⦌C\right)$$
30	19 29	bitri	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \left(\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋2^{nd}\left(a\right)/y⦌C\right)$$
31	30	sbcbii	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋2^{nd}\left(a\right)/y⦌C\right)$$
32		sbcan	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z=⦋2^{nd}\left(a\right)/y⦌C\right)$$
33		sbcan	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)\in B\right)$$
34		sbcel1v	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x\in A\leftrightarrow 1^{st}\left(a\right)\in A$$
35		fvex	$$⊢1^{st}\left(a\right)\in \mathrm{V}$$
36		sbcg	$$⊢1^{st}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)\in B\leftrightarrow 2^{nd}\left(a\right)\in B\right)$$
37	35 36	ax-mp	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)\in B\leftrightarrow 2^{nd}\left(a\right)\in B$$
38	34 37	anbi12i	$$⊢\left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)\in B\right)\leftrightarrow \left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)$$
39	33 38	bitri	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\leftrightarrow \left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)$$
40		sbceq2g	$$⊢1^{st}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z=⦋2^{nd}\left(a\right)/y⦌C\leftrightarrow z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)$$
41	35 40	ax-mp	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z=⦋2^{nd}\left(a\right)/y⦌C\leftrightarrow z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C$$
42	39 41	anbi12i	$$⊢\left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z=⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(\left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)$$
43	31 32 42	3bitri	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \left(\left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)$$
44		sbcan	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z\in D\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x=I\wedge y=J\right)\right)$$
45		sbcg	$$⊢2^{nd}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z\in D\leftrightarrow z\in D\right)$$
46	21 45	ax-mp	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z\in D\leftrightarrow z\in D$$
47		sbcan	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x=I\wedge y=J\right)\leftrightarrow \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x=I\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y=J\right)$$
48		sbcg	$$⊢2^{nd}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x=I\leftrightarrow x=I\right)$$
49	21 48	ax-mp	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x=I\leftrightarrow x=I$$
50		sbceq1g	$$⊢2^{nd}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y=J\leftrightarrow ⦋2^{nd}\left(a\right)/y⦌y=J\right)$$
51	21 50	ax-mp	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y=J\leftrightarrow ⦋2^{nd}\left(a\right)/y⦌y=J$$
52	21	csbvargi	$$⊢⦋2^{nd}\left(a\right)/y⦌y=2^{nd}\left(a\right)$$
53	52	eqeq1i	$$⊢⦋2^{nd}\left(a\right)/y⦌y=J\leftrightarrow 2^{nd}\left(a\right)=J$$
54	51 53	bitri	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y=J\leftrightarrow 2^{nd}\left(a\right)=J$$
55	49 54	anbi12i	$$⊢\left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}x=I\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}y=J\right)\leftrightarrow \left(x=I\wedge 2^{nd}\left(a\right)=J\right)$$
56	47 55	bitri	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x=I\wedge y=J\right)\leftrightarrow \left(x=I\wedge 2^{nd}\left(a\right)=J\right)$$
57	46 56	anbi12i	$$⊢\left(\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}z\in D\wedge \underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(x=I\wedge y=J\right)\right)\leftrightarrow \left(z\in D\wedge \left(x=I\wedge 2^{nd}\left(a\right)=J\right)\right)$$
58	44 57	bitri	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\leftrightarrow \left(z\in D\wedge \left(x=I\wedge 2^{nd}\left(a\right)=J\right)\right)$$
59	58	sbcbii	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge 2^{nd}\left(a\right)=J\right)\right)$$
60		sbcan	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge 2^{nd}\left(a\right)=J\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z\in D\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x=I\wedge 2^{nd}\left(a\right)=J\right)\right)$$
61		sbcg	$$⊢1^{st}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z\in D\leftrightarrow z\in D\right)$$
62	35 61	ax-mp	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z\in D\leftrightarrow z\in D$$
63		sbcan	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x=I\wedge 2^{nd}\left(a\right)=J\right)\leftrightarrow \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x=I\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)=J\right)$$
64		sbceq1g	$$⊢1^{st}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x=I\leftrightarrow ⦋1^{st}\left(a\right)/x⦌x=I\right)$$
65	35 64	ax-mp	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x=I\leftrightarrow ⦋1^{st}\left(a\right)/x⦌x=I$$
66	35	csbvargi	$$⊢⦋1^{st}\left(a\right)/x⦌x=1^{st}\left(a\right)$$
67	66	eqeq1i	$$⊢⦋1^{st}\left(a\right)/x⦌x=I\leftrightarrow 1^{st}\left(a\right)=I$$
68	65 67	bitri	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x=I\leftrightarrow 1^{st}\left(a\right)=I$$
69		sbcg	$$⊢1^{st}\left(a\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)=J\leftrightarrow 2^{nd}\left(a\right)=J\right)$$
70	35 69	ax-mp	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)=J\leftrightarrow 2^{nd}\left(a\right)=J$$
71	68 70	anbi12i	$$⊢\left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}x=I\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}{2}^{nd}\left(a\right)=J\right)\leftrightarrow \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)$$
72	63 71	bitri	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x=I\wedge 2^{nd}\left(a\right)=J\right)\leftrightarrow \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)$$
73	62 72	anbi12i	$$⊢\left(\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}z\in D\wedge \underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\left(x=I\wedge 2^{nd}\left(a\right)=J\right)\right)\leftrightarrow \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)$$
74	59 60 73	3bitri	$$⊢\underset{\dot{}}{[}{1}^{st}\left(a\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(a\right)/y\underset{\dot{}}{]}\left(z\in D\wedge \left(x=I\wedge y=J\right)\right)\leftrightarrow \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)$$
75	18 43 74	3bitr3g	$$⊢\phi \to \left(\left(\left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)\right)$$
76	75	anbi2d	$$⊢\phi \to \left(\left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(\left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\right)\leftrightarrow \left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)\right)\right)$$
77	16 76	syl5bb	$$⊢\phi \to \left(\left(\left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)\right)\right)$$
78		xpss	$$⊢X\times Y\subseteq \mathrm{V}\times \mathrm{V}$$
79		simprr	$$⊢\left(\phi \wedge \left(z\in D\wedge a=⟨I,J⟩\right)\right)\to a=⟨I,J⟩$$
80	9	adantrr	$$⊢\left(\phi \wedge \left(z\in D\wedge a=⟨I,J⟩\right)\right)\to ⟨I,J⟩\in \left(X\times Y\right)$$
81	79 80	eqeltrd	$$⊢\left(\phi \wedge \left(z\in D\wedge a=⟨I,J⟩\right)\right)\to a\in \left(X\times Y\right)$$
82	78 81	sselid	$$⊢\left(\phi \wedge \left(z\in D\wedge a=⟨I,J⟩\right)\right)\to a\in \left(\mathrm{V}\times \mathrm{V}\right)$$
83	82	ex	$$⊢\phi \to \left(\left(z\in D\wedge a=⟨I,J⟩\right)\to a\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
84	83	pm4.71rd	$$⊢\phi \to \left(\left(z\in D\wedge a=⟨I,J⟩\right)\leftrightarrow \left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(z\in D\wedge a=⟨I,J⟩\right)\right)\right)$$
85		eqop	$$⊢a\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left(a=⟨I,J⟩\leftrightarrow \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)$$
86	85	anbi2d	$$⊢a\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left(\left(z\in D\wedge a=⟨I,J⟩\right)\leftrightarrow \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)\right)$$
87	86	pm5.32i	$$⊢\left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(z\in D\wedge a=⟨I,J⟩\right)\right)\leftrightarrow \left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)\right)$$
88	84 87	bitr2di	$$⊢\phi \to \left(\left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(z\in D\wedge \left(1^{st}\left(a\right)=I\wedge 2^{nd}\left(a\right)=J\right)\right)\right)\leftrightarrow \left(z\in D\wedge a=⟨I,J⟩\right)\right)$$
89	77 88	bitrd	$$⊢\phi \to \left(\left(\left(a\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(a\right)\in A\wedge 2^{nd}\left(a\right)\in B\right)\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(z\in D\wedge a=⟨I,J⟩\right)\right)$$
90	15 89	syl5bb	$$⊢\phi \to \left(\left(a\in \left(A\times B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(z\in D\wedge a=⟨I,J⟩\right)\right)$$
91	90	opabbidv	$$⊢\phi \to \left\{⟨z,a⟩|\left(a\in \left(A\times B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\right\}=\left\{⟨z,a⟩|\left(z\in D\wedge a=⟨I,J⟩\right)\right\}$$
92		df-mpo	$$⊢\left(x\in A,y\in B⟼C\right)=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\right\}$$
93	1 92	eqtri	$$⊢F=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\right\}$$
94	93	cnveqi	$$⊢F^{-1}={\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\right\}}^{-1}$$
95		nfv	$$⊢Ⅎi\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)$$
96		nfv	$$⊢Ⅎj\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)$$
97		nfv	$$⊢Ⅎx\left(i\in A\wedge j\in B\right)$$
98		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋i/x⦌⦋j/y⦌C$$
99	98	nfeq2	$$⊢Ⅎxz=⦋i/x⦌⦋j/y⦌C$$
100	97 99	nfan	$$⊢Ⅎx\left(\left(i\in A\wedge j\in B\right)\wedge z=⦋i/x⦌⦋j/y⦌C\right)$$
101		nfv	$$⊢Ⅎy\left(i\in A\wedge j\in B\right)$$
102		nfcv	$$⊢\underset{\_}{Ⅎ}yi$$
103		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋j/y⦌C$$
104	102 103	nfcsbw	$$⊢\underset{\_}{Ⅎ}y⦋i/x⦌⦋j/y⦌C$$
105	104	nfeq2	$$⊢Ⅎyz=⦋i/x⦌⦋j/y⦌C$$
106	101 105	nfan	$$⊢Ⅎy\left(\left(i\in A\wedge j\in B\right)\wedge z=⦋i/x⦌⦋j/y⦌C\right)$$
107		simpl	$$⊢\left(x=i\wedge y=j\right)\to x=i$$
108	107	eleq1d	$$⊢\left(x=i\wedge y=j\right)\to \left(x\in A\leftrightarrow i\in A\right)$$
109		simpr	$$⊢\left(x=i\wedge y=j\right)\to y=j$$
110	109	eleq1d	$$⊢\left(x=i\wedge y=j\right)\to \left(y\in B\leftrightarrow j\in B\right)$$
111	108 110	anbi12d	$$⊢\left(x=i\wedge y=j\right)\to \left(\left(x\in A\wedge y\in B\right)\leftrightarrow \left(i\in A\wedge j\in B\right)\right)$$
112		csbeq1a	$$⊢y=j\to C=⦋j/y⦌C$$
113		csbeq1a	$$⊢x=i\to ⦋j/y⦌C=⦋i/x⦌⦋j/y⦌C$$
114	112 113	sylan9eqr	$$⊢\left(x=i\wedge y=j\right)\to C=⦋i/x⦌⦋j/y⦌C$$
115	114	eqeq2d	$$⊢\left(x=i\wedge y=j\right)\to \left(z=C\leftrightarrow z=⦋i/x⦌⦋j/y⦌C\right)$$
116	111 115	anbi12d	$$⊢\left(x=i\wedge y=j\right)\to \left(\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\leftrightarrow \left(\left(i\in A\wedge j\in B\right)\wedge z=⦋i/x⦌⦋j/y⦌C\right)\right)$$
117	95 96 100 106 116	cbvoprab12	$$⊢\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\right\}=\left\{⟨⟨i,j⟩,z⟩|\left(\left(i\in A\wedge j\in B\right)\wedge z=⦋i/x⦌⦋j/y⦌C\right)\right\}$$
118	117	cnveqi	$$⊢{\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\right\}}^{-1}={\left\{⟨⟨i,j⟩,z⟩|\left(\left(i\in A\wedge j\in B\right)\wedge z=⦋i/x⦌⦋j/y⦌C\right)\right\}}^{-1}$$
119		eleq1	$$⊢a=⟨i,j⟩\to \left(a\in \left(A\times B\right)\leftrightarrow ⟨i,j⟩\in \left(A\times B\right)\right)$$
120		opelxp	$$⊢⟨i,j⟩\in \left(A\times B\right)\leftrightarrow \left(i\in A\wedge j\in B\right)$$
121	119 120	bitrdi	$$⊢a=⟨i,j⟩\to \left(a\in \left(A\times B\right)\leftrightarrow \left(i\in A\wedge j\in B\right)\right)$$
122		csbcom	$$⊢⦋2^{nd}\left(a\right)/j⦌⦋i/x⦌⦋j/y⦌C=⦋i/x⦌⦋2^{nd}\left(a\right)/j⦌⦋j/y⦌C$$
123		csbcow	$$⊢⦋2^{nd}\left(a\right)/j⦌⦋j/y⦌C=⦋2^{nd}\left(a\right)/y⦌C$$
124	123	csbeq2i	$$⊢⦋i/x⦌⦋2^{nd}\left(a\right)/j⦌⦋j/y⦌C=⦋i/x⦌⦋2^{nd}\left(a\right)/y⦌C$$
125	122 124	eqtri	$$⊢⦋2^{nd}\left(a\right)/j⦌⦋i/x⦌⦋j/y⦌C=⦋i/x⦌⦋2^{nd}\left(a\right)/y⦌C$$
126	125	csbeq2i	$$⊢⦋1^{st}\left(a\right)/i⦌⦋2^{nd}\left(a\right)/j⦌⦋i/x⦌⦋j/y⦌C=⦋1^{st}\left(a\right)/i⦌⦋i/x⦌⦋2^{nd}\left(a\right)/y⦌C$$
127		csbcow	$$⊢⦋1^{st}\left(a\right)/i⦌⦋i/x⦌⦋2^{nd}\left(a\right)/y⦌C=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C$$
128	126 127	eqtri	$$⊢⦋1^{st}\left(a\right)/i⦌⦋2^{nd}\left(a\right)/j⦌⦋i/x⦌⦋j/y⦌C=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C$$
129		csbopeq1a	$$⊢a=⟨i,j⟩\to ⦋1^{st}\left(a\right)/i⦌⦋2^{nd}\left(a\right)/j⦌⦋i/x⦌⦋j/y⦌C=⦋i/x⦌⦋j/y⦌C$$
130	128 129	eqtr3id	$$⊢a=⟨i,j⟩\to ⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C=⦋i/x⦌⦋j/y⦌C$$
131	130	eqeq2d	$$⊢a=⟨i,j⟩\to \left(z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\leftrightarrow z=⦋i/x⦌⦋j/y⦌C\right)$$
132	121 131	anbi12d	$$⊢a=⟨i,j⟩\to \left(\left(a\in \left(A\times B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\leftrightarrow \left(\left(i\in A\wedge j\in B\right)\wedge z=⦋i/x⦌⦋j/y⦌C\right)\right)$$
133		xpss	$$⊢A\times B\subseteq \mathrm{V}\times \mathrm{V}$$
134	133	sseli	$$⊢a\in \left(A\times B\right)\to a\in \left(\mathrm{V}\times \mathrm{V}\right)$$
135	134	adantr	$$⊢\left(a\in \left(A\times B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\to a\in \left(\mathrm{V}\times \mathrm{V}\right)$$
136	132 135	cnvoprab	$$⊢{\left\{⟨⟨i,j⟩,z⟩|\left(\left(i\in A\wedge j\in B\right)\wedge z=⦋i/x⦌⦋j/y⦌C\right)\right\}}^{-1}=\left\{⟨z,a⟩|\left(a\in \left(A\times B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\right\}$$
137	94 118 136	3eqtri	$$⊢F^{-1}=\left\{⟨z,a⟩|\left(a\in \left(A\times B\right)\wedge z=⦋1^{st}\left(a\right)/x⦌⦋2^{nd}\left(a\right)/y⦌C\right)\right\}$$
138		df-mpt	$$⊢\left(z\in D⟼⟨I,J⟩\right)=\left\{⟨z,a⟩|\left(z\in D\wedge a=⟨I,J⟩\right)\right\}$$
139	91 137 138	3eqtr4g	$$⊢\phi \to F^{-1}=\left(z\in D⟼⟨I,J⟩\right)$$
140	139	fneq1d	$$⊢\phi \to \left(F^{-1}FnD\leftrightarrow \left(z\in D⟼⟨I,J⟩\right)FnD\right)$$
141	13 140	mpbird	$$⊢\phi \to F^{-1}FnD$$
142		dff1o4	$$⊢F:A\times B\underset{1-1\; onto}{⟶}D\leftrightarrow \left(FFn\left(A\times B\right)\wedge F^{-1}FnD\right)$$
143	7 141 142	sylanbrc	$$⊢\phi \to F:A\times B\underset{1-1\; onto}{⟶}D$$