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 32735

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 3208	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊)
3		f1od2.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 8110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊 → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	syl 17	. 2 ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))
6		f1od2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))
7		opelxpi 5737	. . . . . 6 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8	6, 7	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
9	8	ralrimiva 3152	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10		eqid 2740	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩)
11	10	fnmpt 6720	. . . 4 ⊢ (∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
12	9, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13		elxp7 8065	. . . . . . . 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 3864	. . . . . . . . . . . 12 ⊢ (𝜑 → ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
18	17	sbcbidv 3864	. . . . . . . . . . 11 ⊢ (𝜑 → ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
19		sbcan 3857	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶))
20		sbcan 3857	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵))
21		fvex 6933	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘𝑎) ∈ V
22		sbcg 3883	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
23	21, 22	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
24		sbcel1v 3875	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵 ↔ (2^nd ‘𝑎) ∈ 𝐵)
25	23, 24	anbi12i 627	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
26	20, 25	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
27		sbceq2g 4442	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
28	21, 27	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)
29	26, 28	anbi12i 627	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
30	19, 29	bitri 275	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
31	30	sbcbii 3865	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
32		sbcan 3857	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
33		sbcan 3857	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵))
34		sbcel1v 3875	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ↔ (1^st ‘𝑎) ∈ 𝐴)
35		fvex 6933	. . . . . . . . . . . . . . . 16 ⊢ (1^st ‘𝑎) ∈ V
36		sbcg 3883	. . . . . . . . . . . . . . . 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 627	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
39	33, 38	bitri 275	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
40		sbceq2g 4442	. . . . . . . . . . . . . 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 627	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
43	31, 32, 42	3bitri 297	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
44		sbcan 3857	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))
45		sbcg 3883	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
46	21, 45	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
47		sbcan 3857	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽))
48		sbcg 3883	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼))
49	21, 48	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼)
50		sbceq1g 4440	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽))
51	21, 50	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽)
52	21	csbvargi 4458	. . . . . . . . . . . . . . . . . . 19 ⊢ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = (2^nd ‘𝑎)
53	52	eqeq1i 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
54	51, 53	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
55	49, 54	anbi12i 627	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
56	47, 55	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
57	46, 56	anbi12i 627	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
58	44, 57	bitri 275	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
59	58	sbcbii 3865	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ [(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
60		sbcan 3857	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
61		sbcg 3883	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
62	35, 61	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
63		sbcan 3857	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽))
64		sbceq1g 4440	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼))
65	35, 64	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼)
66	35	csbvargi 4458	. . . . . . . . . . . . . . . . 17 ⊢ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = (1^st ‘𝑎)
67	66	eqeq1i 2745	. . . . . . . . . . . . . . . 16 ⊢ (⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
68	65, 67	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
69		sbcg 3883	. . . . . . . . . . . . . . . 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 627	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
72	63, 71	bitri 275	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
73	62, 72	anbi12i 627	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
74	59, 60, 73	3bitri 297	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
75	18, 43, 74	3bitr3g 313	. . . . . . . . . 10 ⊢ (𝜑 → ((((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
76	75	anbi2d 629	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
77	15, 76	bitrid 283	. . . . . . . 8 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
78		xpss 5716	. . . . . . . . . . . 12 ⊢ (𝑋 × 𝑌) ⊆ (V × V)
79		simprr 772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
80	8	adantrr 716	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
81	79, 80	eqeltrd 2844	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
82	78, 81	sselid 4006	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
83	82	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
84	83	pm4.71rd 562	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩))))
85		eqop 8072	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
86	85	anbi2d 629	. . . . . . . . . 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 288	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
89	77, 88	bitrd 279	. . . . . . 7 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
90	14, 89	bitrid 283	. . . . . 6 ⊢ (𝜑 → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
91	90	opabbidv 5232	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)})
92		df-mpo 7453	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
93	3, 92	eqtri 2768	. . . . . . 7 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
94	93	cnveqi 5899	. . . . . 6 ⊢ ^◡𝐹 = ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
95		nfv 1913	. . . . . . . 8 ⊢ Ⅎ𝑖((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
96		nfv 1913	. . . . . . . 8 ⊢ Ⅎ𝑗((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
97		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
98		nfcsb1v 3946	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
99	98	nfeq2 2926	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
100	97, 99	nfan 1898	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
101		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
102		nfcv 2908	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑖
103		nfcsb1v 3946	. . . . . . . . . . 11 ⊢ Ⅎ𝑦⦋𝑗 / 𝑦⦌𝐶
104	102, 103	nfcsbw 3948	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
105	104	nfeq2 2926	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
106	101, 105	nfan 1898	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
107		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑥 = 𝑖)
108	107	eleq1d 2829	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
109		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑦 = 𝑗)
110	109	eleq1d 2829	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑦 ∈ 𝐵 ↔ 𝑗 ∈ 𝐵))
111	108, 110	anbi12d 631	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
112		csbeq1a 3935	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑦⦌𝐶)
113		csbeq1a 3935	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → ⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
114	112, 113	sylan9eqr 2802	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
115	114	eqeq2d 2751	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
116	111, 115	anbi12d 631	. . . . . . . 8 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
117	95, 96, 100, 106, 116	cbvoprab12 7539	. . . . . . 7 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
118	117	cnveqi 5899	. . . . . 6 ⊢ ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
119		eleq1 2832	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵)))
120		opelxp 5736	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
121	119, 120	bitrdi 287	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
122		csbcom 4443	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶
123		csbcow 3936	. . . . . . . . . . . . . 14 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
124	123	csbeq2i 3929	. . . . . . . . . . . . 13 ⊢ ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
125	122, 124	eqtri 2768	. . . . . . . . . . . 12 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
126	125	csbeq2i 3929	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
127		csbcow 3936	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
128	126, 127	eqtri 2768	. . . . . . . . . 10 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
129		csbopeq1a 8091	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
130	128, 129	eqtr3id 2794	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
131	130	eqeq2d 2751	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
132	121, 131	anbi12d 631	. . . . . . 7 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
133		xpss 5716	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
134	133	sseli 4004	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
135	134	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) → 𝑎 ∈ (V × V))
136	132, 135	cnvoprab 8101	. . . . . 6 ⊢ ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
137	94, 118, 136	3eqtri 2772	. . . . 5 ⊢ ^◡𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
138		df-mpt 5250	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)}
139	91, 137, 138	3eqtr4g 2805	. . . 4 ⊢ (𝜑 → ^◡𝐹 = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩))
140	139	fneq1d 6672	. . 3 ⊢ (𝜑 → (^◡𝐹 Fn 𝐷 ↔ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
141	12, 140	mpbird 257	. 2 ⊢ (𝜑 → ^◡𝐹 Fn 𝐷)
142		dff1o4 6870	. 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 206 ∧ wa 395 = wceq 1537 ∈ wcel 2108 ∀wral 3067 Vcvv 3488 [wsbc 3804 ⦋csb 3921 ⟨cop 4654 {copab 5228 ↦ cmpt 5249 × cxp 5698 ^◡ccnv 5699 Fn wfn 6568 –1-1-onto→wf1o 6572 ‘cfv 6573 {coprab 7449 ∈ cmpo 7450 1^st c1st 8028 2^nd c2nd 8029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-oprab 7452 df-mpo 7453 df-1st 8030 df-2nd 8031

This theorem is referenced by: oddpwdc 34319

W3C validator