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 32733

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 3201	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊)
3		f1od2.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 8095	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑊 → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	syl 17	. 2 ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))
6		f1od2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))
7		opelxpi 5721	. . . . . 6 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8	6, 7	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
9	8	ralrimiva 3145	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10		eqid 2736	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩)
11	10	fnmpt 6707	. . . 4 ⊢ (∀𝑧 ∈ 𝐷 ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
12	9, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13		elxp7 8050	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ (V × V) ∧ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵)))
14	13	anbi1i 624	. . . . . . 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 3844	. . . . . . . . . . . 12 ⊢ (𝜑 → ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
18	17	sbcbidv 3844	. . . . . . . . . . 11 ⊢ (𝜑 → ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))
19		sbcan 3837	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ [(2^nd ‘𝑎) / 𝑦]𝑧 = 𝐶))
20		sbcan 3837	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵))
21		fvex 6918	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘𝑎) ∈ V
22		sbcg 3862	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
23	21, 22	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
24		sbcel1v 3855	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵 ↔ (2^nd ‘𝑎) ∈ 𝐵)
25	23, 24	anbi12i 628	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 ∈ 𝐴 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
26	20, 25	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
27		sbceq2g 4418	. . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
31	30	sbcbii 3845	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ [(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
32		sbcan 3837	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥]((𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ [(1^st ‘𝑎) / 𝑥]𝑧 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
33		sbcan 3837	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) ∈ 𝐵))
34		sbcel1v 3855	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 ∈ 𝐴 ↔ (1^st ‘𝑎) ∈ 𝐴)
35		fvex 6918	. . . . . . . . . . . . . . . 16 ⊢ (1^st ‘𝑎) ∈ V
36		sbcg 3862	. . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ↔ ((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵))
40		sbceq2g 4418	. . . . . . . . . . . . . 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 297	. . . . . . . . . . 11 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦]((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (((1^st ‘𝑎) ∈ 𝐴 ∧ (2^nd ‘𝑎) ∈ 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶))
44		sbcan 3837	. . . . . . . . . . . . . 14 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))
45		sbcg 3862	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
46	21, 45	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
47		sbcan 3837	. . . . . . . . . . . . . . . 16 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽))
48		sbcg 3862	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼))
49	21, 48	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ↔ 𝑥 = 𝐼)
50		sbceq1g 4416	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑎) ∈ V → ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽))
51	21, 50	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽)
52	21	csbvargi 4434	. . . . . . . . . . . . . . . . . . 19 ⊢ ⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = (2^nd ‘𝑎)
53	52	eqeq1i 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(2^nd ‘𝑎) / 𝑦⦌𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
54	51, 53	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ ([(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2^nd ‘𝑎) = 𝐽)
55	49, 54	anbi12i 628	. . . . . . . . . . . . . . . 16 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑥 = 𝐼 ∧ [(2^nd ‘𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
56	47, 55	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽))
57	46, 56	anbi12i 628	. . . . . . . . . . . . . 14 ⊢ (([(2^nd ‘𝑎) / 𝑦]𝑧 ∈ 𝐷 ∧ [(2^nd ‘𝑎) / 𝑦](𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
58	44, 57	bitri 275	. . . . . . . . . . . . 13 ⊢ ([(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
59	58	sbcbii 3845	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥][(2^nd ‘𝑎) / 𝑦](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) ↔ [(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
60		sbcan 3837	. . . . . . . . . . . 12 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)) ↔ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ∧ [(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
61		sbcg 3862	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
62	35, 61	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷)
63		sbcan 3837	. . . . . . . . . . . . . 14 ⊢ ([(1^st ‘𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽) ↔ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ∧ [(1^st ‘𝑎) / 𝑥](2^nd ‘𝑎) = 𝐽))
64		sbceq1g 4416	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑎) ∈ V → ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼))
65	35, 64	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼)
66	35	csbvargi 4434	. . . . . . . . . . . . . . . . 17 ⊢ ⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = (1^st ‘𝑎)
67	66	eqeq1i 2741	. . . . . . . . . . . . . . . 16 ⊢ (⦋(1^st ‘𝑎) / 𝑥⦌𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
68	65, 67	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([(1^st ‘𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1^st ‘𝑎) = 𝐼)
69		sbcg 3862	. . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . 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 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 630	. . . . . . . . 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 5700	. . . . . . . . . . . 12 ⊢ (𝑋 × 𝑌) ⊆ (V × V)
79		simprr 772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
80	8	adantrr 717	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
81	79, 80	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
82	78, 81	sselid 3980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
83	82	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
84	83	pm4.71rd 562	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩))))
85		eqop 8057	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1^st ‘𝑎) = 𝐼 ∧ (2^nd ‘𝑎) = 𝐽)))
86	85	anbi2d 630	. . . . . . . . . 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 5208	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)})
92		df-mpo 7437	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
93	3, 92	eqtri 2764	. . . . . . 7 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
94	93	cnveqi 5884	. . . . . 6 ⊢ ^◡𝐹 = ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
95		nfv 1913	. . . . . . . 8 ⊢ Ⅎ𝑖((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
96		nfv 1913	. . . . . . . 8 ⊢ Ⅎ𝑗((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
97		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
98		nfcsb1v 3922	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
99	98	nfeq2 2922	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
100	97, 99	nfan 1898	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
101		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)
102		nfcv 2904	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑖
103		nfcsb1v 3922	. . . . . . . . . . 11 ⊢ Ⅎ𝑦⦋𝑗 / 𝑦⦌𝐶
104	102, 103	nfcsbw 3924	. . . . . . . . . 10 ⊢ Ⅎ𝑦⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
105	104	nfeq2 2922	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶
106	101, 105	nfan 1898	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
107		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑥 = 𝑖)
108	107	eleq1d 2825	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
109		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝑦 = 𝑗)
110	109	eleq1d 2825	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑦 ∈ 𝐵 ↔ 𝑗 ∈ 𝐵))
111	108, 110	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
112		csbeq1a 3912	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑦⦌𝐶)
113		csbeq1a 3912	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → ⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
114	112, 113	sylan9eqr 2798	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → 𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
115	114	eqeq2d 2747	. . . . . . . . 9 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
116	111, 115	anbi12d 632	. . . . . . . 8 ⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
117	95, 96, 100, 106, 116	cbvoprab12 7523	. . . . . . 7 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
118	117	cnveqi 5884	. . . . . 6 ⊢ ^◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)}
119		eleq1 2828	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵)))
120		opelxp 5720	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
121	119, 120	bitrdi 287	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
122		csbcom 4419	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶
123		csbcow 3913	. . . . . . . . . . . . . 14 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
124	123	csbeq2i 3906	. . . . . . . . . . . . 13 ⊢ ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
125	122, 124	eqtri 2764	. . . . . . . . . . . 12 ⊢ ⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
126	125	csbeq2i 3906	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
127		csbcow 3913	. . . . . . . . . . 11 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋𝑖 / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
128	126, 127	eqtri 2764	. . . . . . . . . 10 ⊢ ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶
129		csbopeq1a 8076	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑖⦌⦋(2^nd ‘𝑎) / 𝑗⦌⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
130	128, 129	eqtr3id 2790	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)
131	130	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶))
132	121, 131	anbi12d 632	. . . . . . 7 ⊢ (𝑎 = ⟨𝑖, 𝑗⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)))
133		xpss 5700	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
134	133	sseli 3978	. . . . . . . 8 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
135	134	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶) → 𝑎 ∈ (V × V))
136	132, 135	cnvoprab 8086	. . . . . 6 ⊢ ^◡{⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑧 = ⦋𝑖 / 𝑥⦌⦋𝑗 / 𝑦⦌𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
137	94, 118, 136	3eqtri 2768	. . . . 5 ⊢ ^◡𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = ⦋(1^st ‘𝑎) / 𝑥⦌⦋(2^nd ‘𝑎) / 𝑦⦌𝐶)}
138		df-mpt 5225	. . . . 5 ⊢ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧 ∈ 𝐷 ∧ 𝑎 = ⟨𝐼, 𝐽⟩)}
139	91, 137, 138	3eqtr4g 2801	. . . 4 ⊢ (𝜑 → ^◡𝐹 = (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩))
140	139	fneq1d 6660	. . 3 ⊢ (𝜑 → (^◡𝐹 Fn 𝐷 ↔ (𝑧 ∈ 𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
141	12, 140	mpbird 257	. 2 ⊢ (𝜑 → ^◡𝐹 Fn 𝐷)
142		dff1o4 6855	. 2 ⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ^◡𝐹 Fn 𝐷))
143	5, 141, 142	sylanbrc 583	1 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∀wral 3060 Vcvv 3479 [wsbc 3787 ⦋csb 3898 ⟨cop 4631 {copab 5204 ↦ cmpt 5224 × cxp 5682 ^◡ccnv 5683 Fn wfn 6555 –1-1-onto→wf1o 6559 ‘cfv 6560 {coprab 7433 ∈ cmpo 7434 1^st c1st 8013 2^nd c2nd 8014

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 ax-un 7756

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-oprab 7436 df-mpo 7437 df-1st 8015 df-2nd 8016

This theorem is referenced by: oddpwdc 34357

W3C validator