f1od2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > f1od2		Structured version Visualization version GIF version

Theorem f1od2 30958

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

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

**Assertion**
Ref	Expression
f1od2	⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)

Distinct variable groups: 𝑥,𝑦,𝑧,𝐴 𝑥,𝐵,𝑦,𝑧 𝑧,𝐶 𝑥,𝐷,𝑦,𝑧 𝑥,𝐼,𝑦 𝑥,𝐽,𝑦 𝜑,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐶(𝑥,𝑦) 𝐹(𝑥,𝑦,𝑧) 𝐼(𝑧) 𝐽(𝑧) 𝑊(𝑥,𝑦,𝑧) 𝑋(𝑥,𝑦,𝑧) 𝑌(𝑥,𝑦,𝑧)

Proof of Theorem f1od2 Dummy variables 𝑖 𝑎 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1od2.2	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑊)
2	1	ralrimivva 3114	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊)
3		f1od2.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 7882	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊 → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	syl 17	. 2 ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))
6		f1od2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))
7		opelxpi 5617	. . . . . 6 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8	6, 7	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
9	8	ralrimiva 3107	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10		eqid 2738	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩)
11	10	fnmpt 6557	. . . 4 ⊢ (∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
12	9, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13		elxp7 7839	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)))
14	13	anbi1i 623	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
15		anass 468	. . . . . . . . 9 ⊢ (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑎 ∈ (V × V) ∧ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)))
16		f1od2.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
17	16	sbcbidv 3770	. . . . . . . . . . . 12 ⊢ (𝜑 → ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
18	17	sbcbidv 3770	. . . . . . . . . . 11 ⊢ (𝜑 → ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
19		sbcan 3763	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶))
20		sbcan 3763	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵))
21		fvex 6769	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘𝑎) ∈ V
22		sbcg 3791	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
23	21, 22	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
24		sbcel1v 3783	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵 ↔ (2^nd ‘𝑎) ∈ 𝐵)
25	23, 24	anbi12i 626	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
26	20, 25	bitri 274	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
27		sbceq2g 4347	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
28	21, 27	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)
29	26, 28	anbi12i 626	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
30	19, 29	bitri 274	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
31	30	sbcbii 3772	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
32		sbcan 3763	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
33		sbcan 3763	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵))
34		sbcel1v 3783	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ↔ (1^st ‘𝑎) ∈ 𝐴)
35		fvex 6769	. . . . . . . . . . . . . . . 16 ⊢ (1^st ‘𝑎) ∈ V
36		sbcg 3791	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵 ↔ (2^nd ‘𝑎) ∈ 𝐵))
37	35, 36	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵 ↔ (2^nd ‘𝑎) ∈ 𝐵)
38	34, 37	anbi12i 626	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
39	33, 38	bitri 274	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
40		sbceq2g 4347	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
41	35, 40	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)
42	39, 41	anbi12i 626	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
43	31, 32, 42	3bitri 296	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
44		sbcan 3763	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))
45		sbcg 3791	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
46	21, 45	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
47		sbcan 3763	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽))
48		sbcg 3791	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼))
49	21, 48	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼)
50		sbceq1g 4345	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽))
51	21, 50	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽)
52	21	csbvargi 4363	. . . . . . . . . . . . . . . . . . 19 ⊢ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = (2^nd ‘𝑎)
53	52	eqeq1i 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
54	51, 53	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
55	49, 54	anbi12i 626	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
56	47, 55	bitri 274	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
57	46, 56	anbi12i 626	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
58	44, 57	bitri 274	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
59	58	sbcbii 3772	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ [(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
60		sbcan 3763	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
61		sbcg 3791	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
62	35, 61	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
63		sbcan 3763	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽))
64		sbceq1g 4345	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼))
65	35, 64	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼)
66	35	csbvargi 4363	. . . . . . . . . . . . . . . . 17 ⊢ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = (1^st ‘𝑎)
67	66	eqeq1i 2743	. . . . . . . . . . . . . . . 16 ⊢ (⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
68	65, 67	bitri 274	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
69		sbcg 3791	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽))
70	35, 69	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
71	68, 70	anbi12i 626	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
72	63, 71	bitri 274	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
73	62, 72	anbi12i 626	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
74	59, 60, 73	3bitri 296	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
75	18, 43, 74	3bitr3g 312	. . . . . . . . . 10 ⊢ (𝜑 → ((((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
76	75	anbi2d 628	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
77	15, 76	syl5bb 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
78		xpss 5596	. . . . . . . . . . . 12 ⊢ (𝑋 × 𝑌) ⊆ (V × V)
79		simprr 769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
80	8	adantrr 713	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
81	79, 80	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
82	78, 81	sselid 3915	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
83	82	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
84	83	pm4.71rd 562	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩))))
85		eqop 7846	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
86	85	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑎 ∈ (V × V) → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
87	86	pm5.32i 574	. . . . . . . . 9 ⊢ ((𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
88	84, 87	bitr2di 287	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
89	77, 88	bitrd 278	. . . . . . 7 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
90	14, 89	syl5bb 282	. . . . . 6 ⊢ (𝜑 → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
91	90	opabbidv 5136	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)})
92		df-mpo 7260	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
93	3, 92	eqtri 2766	. . . . . . 7 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
94	93	cnveqi 5772	. . . . . 6 ⊢ ^◡𝐹 = ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
95		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑖((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
96		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑗((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
97		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
98		nfcsb1v 3853	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
99	98	nfeq2 2923	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
100	97, 99	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
101		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
102		nfcv 2906	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑖
103		nfcsb1v 3853	. . . . . . . . . . 11 ⊢ Ⅎ𝑦⦋𝑗 / 𝑦⦌𝐶
104	102, 103	nfcsbw 3855	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
105	104	nfeq2 2923	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
106	101, 105	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
107		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑥 = 𝑖)
108	107	eleq1d 2823	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
109		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑦 = 𝑗)
110	109	eleq1d 2823	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑦 ∈ 𝐵 ↔ 𝑗 ∈ 𝐵))
111	108, 110	anbi12d 630	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
112		csbeq1a 3842	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑦⦌𝐶)
113		csbeq1a 3842	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → ⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
114	112, 113	sylan9eqr 2801	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
115	114	eqeq2d 2749	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
116	111, 115	anbi12d 630	. . . . . . . 8 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
117	95, 96, 100, 106, 116	cbvoprab12 7342	. . . . . . 7 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
118	117	cnveqi 5772	. . . . . 6 ⊢ ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
119		eleq1 2826	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵)))
120		opelxp 5616	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
121	119, 120	bitrdi 286	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
122		csbcom 4348	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶
123		csbcow 3843	. . . . . . . . . . . . . 14 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
124	123	csbeq2i 3836	. . . . . . . . . . . . 13 ⊢ ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
125	122, 124	eqtri 2766	. . . . . . . . . . . 12 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
126	125	csbeq2i 3836	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
127		csbcow 3843	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
128	126, 127	eqtri 2766	. . . . . . . . . 10 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
129		csbopeq1a 7864	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
130	128, 129	eqtr3id 2793	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
131	130	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
132	121, 131	anbi12d 630	. . . . . . 7 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
133		xpss 5596	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
134	133	sseli 3913	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
135	134	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) → 𝑎 ∈ (V × V))
136	132, 135	cnvoprab 7873	. . . . . 6 ⊢ ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
137	94, 118, 136	3eqtri 2770	. . . . 5 ⊢ ^◡𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
138		df-mpt 5154	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)}
139	91, 137, 138	3eqtr4g 2804	. . . 4 ⊢ (𝜑 → ^◡𝐹 = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩))
140	139	fneq1d 6510	. . 3 ⊢ (𝜑 → (^◡𝐹 Fn 𝐷 ↔ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
141	12, 140	mpbird 256	. 2 ⊢ (𝜑 → ^◡𝐹 Fn 𝐷)
142		dff1o4 6708	. 2 ⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ^◡𝐹 Fn 𝐷))
143	5, 141, 142	sylanbrc 582	1 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∀wral 3063 Vcvv 3422 [wsbc 3711 ⦋csb 3828 ⟨cop 4564 {copab 5132 ↦ cmpt 5153 × cxp 5578 ^◡ccnv 5579 Fn wfn 6413 –1-1-onto→wf1o 6417 ‘cfv 6418 {coprab 7256 ∈ cmpo 7257 1^st c1st 7802 2^nd c2nd 7803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-oprab 7259 df-mpo 7260 df-1st 7804 df-2nd 7805

This theorem is referenced by: oddpwdc 32221

W3C validator