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 33045

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 8067	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊 → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	syl 18	. 2 ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))
6		f1od2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))
7		opelxpi 5700	. . . . . 6 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8	6, 7	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
9	8	ralrimiva 3157	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10		eqid 2763	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩)
11	10	fnmpt 6677	. . . 4 ⊢ (∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
12	9, 11	syl 18	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13		elxp7 8022	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)))
14	13	anbi1i 635	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
15		anass 473	. . . . . . . . 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 3800	. . . . . . . . . . . 12 ⊢ (𝜑 → ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
18	17	sbcbidv 3800	. . . . . . . . . . 11 ⊢ (𝜑 → ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
19		sbcan 3794	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶))
20		sbcan 3794	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵))
21		fvex 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘𝑎) ∈ V
22		sbcg 3817	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
23	21, 22	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
24		sbcel1v 3810	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵 ↔ (2^nd ‘𝑎) ∈ 𝐵)
25	23, 24	anbi12i 639	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
26	20, 25	bitri 278	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
27		sbceq2g 4385	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
28	21, 27	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)
29	26, 28	anbi12i 639	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
30	19, 29	bitri 278	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
31	30	sbcbii 3801	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
32		sbcan 3794	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
33		sbcan 3794	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵))
34		sbcel1v 3810	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ↔ (1^st ‘𝑎) ∈ 𝐴)
35		fvex 6896	. . . . . . . . . . . . . . . 16 ⊢ (1^st ‘𝑎) ∈ V
36		sbcg 3817	. . . . . . . . . . . . . . . 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 639	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
39	33, 38	bitri 278	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
40		sbceq2g 4385	. . . . . . . . . . . . . 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 639	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
43	31, 32, 42	3bitri 300	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
44		sbcan 3794	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))
45		sbcg 3817	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
46	21, 45	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
47		sbcan 3794	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽))
48		sbcg 3817	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼))
49	21, 48	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼)
50		sbceq1g 4383	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽))
51	21, 50	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽)
52	21	csbvargi 4401	. . . . . . . . . . . . . . . . . . 19 ⊢ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = (2^nd ‘𝑎)
53	52	eqeq1i 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
54	51, 53	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
55	49, 54	anbi12i 639	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
56	47, 55	bitri 278	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
57	46, 56	anbi12i 639	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
58	44, 57	bitri 278	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
59	58	sbcbii 3801	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ [(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
60		sbcan 3794	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
61		sbcg 3817	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
62	35, 61	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
63		sbcan 3794	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽))
64		sbceq1g 4383	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼))
65	35, 64	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼)
66	35	csbvargi 4401	. . . . . . . . . . . . . . . . 17 ⊢ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = (1^st ‘𝑎)
67	66	eqeq1i 2768	. . . . . . . . . . . . . . . 16 ⊢ (⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
68	65, 67	bitri 278	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
69		sbcg 3817	. . . . . . . . . . . . . . . 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 639	. . . . . . . . . . . . . 14 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
72	63, 71	bitri 278	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
73	62, 72	anbi12i 639	. . . . . . . . . . . 12 ⊢ (([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
74	59, 60, 73	3bitri 300	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
75	18, 43, 74	3bitr3g 316	. . . . . . . . . 10 ⊢ (𝜑 → ((((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
76	75	anbi2d 641	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
77	15, 76	bitrid 286	. . . . . . . 8 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))))
78		xpss 5679	. . . . . . . . . . . 12 ⊢ (𝑋 × 𝑌) ⊆ (V × V)
79		simprr 784	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
80	8	adantrr 729	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
81	79, 80	eqeltrd 2863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
82	78, 81	sselid 3936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
83	82	ex 417	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
84	83	pm4.71rd 571	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩))))
85		eqop 8029	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
86	85	anbi2d 641	. . . . . . . . . 10 ⊢ (𝑎 ∈ (V × V) → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
87	86	pm5.32i 584	. . . . . . . . 9 ⊢ ((𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))))
88	84, 87	bitr2di 291	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
89	77, 88	bitrd 282	. . . . . . 7 ⊢ (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
90	14, 89	bitrid 286	. . . . . 6 ⊢ (𝜑 → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)))
91	90	opabbidv 5178	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)})
92		df-mpo 7417	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
93	3, 92	eqtri 2786	. . . . . . 7 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
94	93	cnveqi 5862	. . . . . 6 ⊢ ^◡𝐹 = ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
95		nfv 1944	. . . . . . . 8 ⊢ Ⅎ𝑖((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
96		nfv 1944	. . . . . . . 8 ⊢ Ⅎ𝑗((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
97		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
98		nfcsb1v 3878	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
99	98	nfeq2 2942	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
100	97, 99	nfan 1929	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
101		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
102		nfcv 2925	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑖
103		nfcsb1v 3878	. . . . . . . . . . 11 ⊢ Ⅎ𝑦⦋𝑗 / 𝑦⦌𝐶
104	102, 103	nfcsbw 3880	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
105	104	nfeq2 2942	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
106	101, 105	nfan 1929	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
107		simpl 487	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑥 = 𝑖)
108	107	eleq1d 2848	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
109		simpr 489	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑦 = 𝑗)
110	109	eleq1d 2848	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑦 ∈ 𝐵 ↔ 𝑗 ∈ 𝐵))
111	108, 110	anbi12d 643	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
112		csbeq1a 3868	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑦⦌𝐶)
113		csbeq1a 3868	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → ⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
114	112, 113	sylan9eqr 2820	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
115	114	eqeq2d 2774	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
116	111, 115	anbi12d 643	. . . . . . . 8 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
117	95, 96, 100, 106, 116	cbvoprab12 7501	. . . . . . 7 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
118	117	cnveqi 5862	. . . . . 6 ⊢ ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
119		eleq1 2851	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵)))
120		opelxp 5699	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
121	119, 120	bitrdi 290	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
122		csbcom 4386	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶
123		csbcow 3869	. . . . . . . . . . . . . 14 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
124	123	csbeq2i 3862	. . . . . . . . . . . . 13 ⊢ ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
125	122, 124	eqtri 2786	. . . . . . . . . . . 12 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
126	125	csbeq2i 3862	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
127		csbcow 3869	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
128	126, 127	eqtri 2786	. . . . . . . . . 10 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
129		csbopeq1a 8048	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
130	128, 129	eqtr3id 2812	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
131	130	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
132	121, 131	anbi12d 643	. . . . . . 7 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
133		xpss 5679	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
134	133	sseli 3934	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
135	134	adantr 485	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) → 𝑎 ∈ (V × V))
136	132, 135	cnvoprab 8058	. . . . . 6 ⊢ ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
137	94, 118, 136	3eqtri 2790	. . . . 5 ⊢ ^◡𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
138		df-mpt 5194	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)}
139	91, 137, 138	3eqtr4g 2823	. . . 4 ⊢ (𝜑 → ^◡𝐹 = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩))
140	139	fneq1d 6630	. . 3 ⊢ (𝜑 → (^◡𝐹 Fn 𝐷 ↔ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
141	12, 140	mpbird 260	. 2 ⊢ (𝜑 → ^◡𝐹 Fn 𝐷)
142		dff1o4 6831	. 2 ⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ^◡𝐹 Fn 𝐷))
143	5, 141, 142	sylanbrc 594	1 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ∀wral 3079 Vcvv 3455 [wsbc 3745 ⦋csb 3854 ⟨cop 4596 {copab 5174 ↦ cmpt 5193 × cxp 5661 ^◡ccnv 5662 Fn wfn 6533 –1-1-onto→wf1o 6537 ‘cfv 6538 {coprab 7413 ∈ cmpo 7414 1^st c1st 7985 2^nd c2nd 7986

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pr 5406 ax-un 7734

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4489 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-oprab 7416 df-mpo 7417 df-1st 7987 df-2nd 7988

This theorem is referenced by: oddpwdc 34725

W3C validator