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 30451

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 3191	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊)
3		f1od2.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 7761	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊 → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	syl 17	. 2 ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))
6		f1od2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))
7		opelxpi 5587	. . . . . 6 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8	6, 7	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
9	8	ralrimiva 3182	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10		eqid 2821	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩)
11	10	fnmpt 6483	. . . 4 ⊢ (∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
12	9, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13		elxp7 7718	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)))
14	13	anbi1i 625	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
15		anass 471	. . . . . . . . 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 3827	. . . . . . . . . . . 12 ⊢ (𝜑 → ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
18	17	sbcbidv 3827	. . . . . . . . . . 11 ⊢ (𝜑 → ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
19		sbcan 3821	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶))
20		sbcan 3821	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵))
21		fvex 6678	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘𝑎) ∈ V
22		sbcg 3847	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
23	21, 22	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
24		sbcel1v 3839	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵 ↔ (2^nd ‘𝑎) ∈ 𝐵)
25	23, 24	anbi12i 628	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
26	20, 25	bitri 277	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
27		sbceq2g 4368	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
28	21, 27	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)
29	26, 28	anbi12i 628	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
30	19, 29	bitri 277	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
31	30	sbcbii 3829	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
32		sbcan 3821	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
33		sbcan 3821	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵))
34		sbcel1v 3839	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ↔ (1^st ‘𝑎) ∈ 𝐴)
35		fvex 6678	. . . . . . . . . . . . . . . 16 ⊢ (1^st ‘𝑎) ∈ V
36		sbcg 3847	. . . . . . . . . . . . . . . 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 628	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
39	33, 38	bitri 277	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
40		sbceq2g 4368	. . . . . . . . . . . . . 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 628	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
43	31, 32, 42	3bitri 299	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
44		sbcan 3821	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))
45		sbcg 3847	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
46	21, 45	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
47		sbcan 3821	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽))
48		sbcg 3847	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼))
49	21, 48	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼)
50		sbceq1g 4366	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽))
51	21, 50	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽)
52	21	csbvargi 4384	. . . . . . . . . . . . . . . . . . 19 ⊢ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = (2^nd ‘𝑎)
53	52	eqeq1i 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
54	51, 53	bitri 277	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
55	49, 54	anbi12i 628	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
56	47, 55	bitri 277	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
57	46, 56	anbi12i 628	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
58	44, 57	bitri 277	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
59	58	sbcbii 3829	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ [(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
60		sbcan 3821	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
61		sbcg 3847	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
62	35, 61	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
63		sbcan 3821	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽))
64		sbceq1g 4366	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼))
65	35, 64	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼)
66	35	csbvargi 4384	. . . . . . . . . . . . . . . . 17 ⊢ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = (1^st ‘𝑎)
67	66	eqeq1i 2826	. . . . . . . . . . . . . . . 16 ⊢ (⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
68	65, 67	bitri 277	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
69		sbcg 3847	. . . . . . . . . . . . . . . 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 628	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
72	63, 71	bitri 277	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
73	62, 72	anbi12i 628	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
74	59, 60, 73	3bitri 299	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
75	18, 43, 74	3bitr3g 315	. . . . . . . . . 10 ⊢ (𝜑 → ((((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
76	75	anbi2d 630	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
77	15, 76	syl5bb 285	. . . . . . . 8 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
78		xpss 5566	. . . . . . . . . . . 12 ⊢ (𝑋 × 𝑌) ⊆ (V × V)
79		simprr 771	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
80	8	adantrr 715	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
81	79, 80	eqeltrd 2913	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
82	78, 81	sseldi 3965	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
83	82	ex 415	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
84	83	pm4.71rd 565	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩))))
85		eqop 7725	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
86	85	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑎 ∈ (V × V) → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
87	86	pm5.32i 577	. . . . . . . . 9 ⊢ ((𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
88	84, 87	syl6rbb 290	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
89	77, 88	bitrd 281	. . . . . . 7 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
90	14, 89	syl5bb 285	. . . . . 6 ⊢ (𝜑 → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
91	90	opabbidv 5125	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)})
92		df-mpo 7155	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
93	3, 92	eqtri 2844	. . . . . . 7 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
94	93	cnveqi 5740	. . . . . 6 ⊢ ^◡𝐹 = ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
95		nfv 1911	. . . . . . . 8 ⊢ Ⅎ𝑖((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
96		nfv 1911	. . . . . . . 8 ⊢ Ⅎ𝑗((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
97		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
98		nfcsb1v 3907	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
99	98	nfeq2 2995	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
100	97, 99	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
101		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
102		nfcv 2977	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑖
103		nfcsb1v 3907	. . . . . . . . . . 11 ⊢ Ⅎ𝑦⦋𝑗 / 𝑦⦌𝐶
104	102, 103	nfcsbw 3909	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
105	104	nfeq2 2995	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
106	101, 105	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
107		simpl 485	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑥 = 𝑖)
108	107	eleq1d 2897	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
109		simpr 487	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑦 = 𝑗)
110	109	eleq1d 2897	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑦 ∈ 𝐵 ↔ 𝑗 ∈ 𝐵))
111	108, 110	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
112		csbeq1a 3897	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑦⦌𝐶)
113		csbeq1a 3897	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → ⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
114	112, 113	sylan9eqr 2878	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
115	114	eqeq2d 2832	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
116	111, 115	anbi12d 632	. . . . . . . 8 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
117	95, 96, 100, 106, 116	cbvoprab12 7237	. . . . . . 7 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
118	117	cnveqi 5740	. . . . . 6 ⊢ ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
119		eleq1 2900	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵)))
120		opelxp 5586	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
121	119, 120	syl6bb 289	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
122		csbcom 4369	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶
123		csbcow 3898	. . . . . . . . . . . . . 14 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
124	123	csbeq2i 3891	. . . . . . . . . . . . 13 ⊢ ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
125	122, 124	eqtri 2844	. . . . . . . . . . . 12 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
126	125	csbeq2i 3891	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
127		csbcow 3898	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
128	126, 127	eqtri 2844	. . . . . . . . . 10 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
129		csbopeq1a 7743	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
130	128, 129	syl5eqr 2870	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
131	130	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
132	121, 131	anbi12d 632	. . . . . . 7 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
133		xpss 5566	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
134	133	sseli 3963	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
135	134	adantr 483	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) → 𝑎 ∈ (V × V))
136	132, 135	cnvoprab 7752	. . . . . 6 ⊢ ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
137	94, 118, 136	3eqtri 2848	. . . . 5 ⊢ ^◡𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
138		df-mpt 5140	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)}
139	91, 137, 138	3eqtr4g 2881	. . . 4 ⊢ (𝜑 → ^◡𝐹 = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩))
140	139	fneq1d 6441	. . 3 ⊢ (𝜑 → (^◡𝐹 Fn 𝐷 ↔ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
141	12, 140	mpbird 259	. 2 ⊢ (𝜑 → ^◡𝐹 Fn 𝐷)
142		dff1o4 6618	. 2 ⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ^◡𝐹 Fn 𝐷))
143	5, 141, 142	sylanbrc 585	1 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ∀wral 3138 Vcvv 3495 [wsbc 3772 ⦋csb 3883 ⟨cop 4567 {copab 5121 ↦ cmpt 5139 × cxp 5548 ^◡ccnv 5549 Fn wfn 6345 –1-1-onto→wf1o 6349 ‘cfv 6350 {coprab 7151 ∈ cmpo 7152 1^st c1st 7681 2^nd c2nd 7682

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-id 5455 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-oprab 7154 df-mpo 7155 df-1st 7683 df-2nd 7684

This theorem is referenced by: oddpwdc 31607

W3C validator