Theorem fcoresf1 48138

Description: If a composition is injective, then the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 18-Sep-2024.) (Revised by AV, 7-Oct-2024.)

Hypotheses

Ref	Expression
fcores.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fcores.e	⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)
fcores.p	⊢ 𝑃 = (◡𝐹 “ 𝐶)
fcores.x	⊢ 𝑋 = (𝐹 ↾ 𝑃)
fcores.g	⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
fcores.y	⊢ 𝑌 = (𝐺 ↾ 𝐸)
fcoresf1.i	⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷)

Assertion

Ref	Expression
fcoresf1	⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))

Proof of Theorem fcoresf1

Dummy variables 𝑥 𝑦 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fcores.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fcores.e	. . . . 5 ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)
3		fcores.p	. . . . 5 ⊢ 𝑃 = (◡𝐹 “ 𝐶)
4		fcores.x	. . . . 5 ⊢ 𝑋 = (𝐹 ↾ 𝑃)
5	1, 2, 3, 4	fcoreslem3 48134	. . . 4 ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸)
6		fof 6796	. . . 4 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋:𝑃⟶𝐸)
7	5, 6	syl 18	. . 3 ⊢ (𝜑 → 𝑋:𝑃⟶𝐸)
8		fcoresf1.i	. . . 4 ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷)
9		dff13 7258	. . . . 5 ⊢ ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ ((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)))
10		fcores.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
11		fcores.y	. . . . . . . . . . . 12 ⊢ 𝑌 = (𝐺 ↾ 𝐸)
12	1, 2, 3, 4, 10, 11	fcoresf1lem 48137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
13	12	adantrr 730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
14	1, 2, 3, 4, 10, 11	fcoresf1lem 48137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
15	14	adantrl 729	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
16	13, 15	eqeq12d 2777	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
17	16	imbi1d 344	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ ((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦)))
18		fveq2 6885	. . . . . . . . . 10 ⊢ ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)))
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
20	19	imim1d 83	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
21	17, 20	sylbid 243	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
22	21	ralimdvva 3210	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
23	22	adantld 496	. . . . 5 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
24	9, 23	biimtrid 245	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
25	8, 24	mpd 16	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦))
26		dff13 7258	. . 3 ⊢ (𝑋:𝑃–1-1→𝐸 ↔ (𝑋:𝑃⟶𝐸 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
27	7, 25, 26	sylanbrc 595	. 2 ⊢ (𝜑 → 𝑋:𝑃–1-1→𝐸)
28	2	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐶))
29		inss2 4183	. . . . . 6 ⊢ (ran 𝐹 ∩ 𝐶) ⊆ 𝐶
30	28, 29	eqsstrdi 3975	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ 𝐶)
31	10, 30	fssresd 6749	. . . 4 ⊢ (𝜑 → (𝐺 ↾ 𝐸):𝐸⟶𝐷)
32	11	feq1i 6700	. . . 4 ⊢ (𝑌:𝐸⟶𝐷 ↔ (𝐺 ↾ 𝐸):𝐸⟶𝐷)
33	31, 32	sylibr 237	. . 3 ⊢ (𝜑 → 𝑌:𝐸⟶𝐷)
34	1, 2, 3, 4	fcoreslem2 48133	. . . . . . . . 9 ⊢ (𝜑 → ran 𝑋 = 𝐸)
35	34	eqcomd 2767	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = ran 𝑋)
36	35	eleq2d 2847	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ 𝑥 ∈ ran 𝑋))
37		fofn 6798	. . . . . . . . 9 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋 Fn 𝑃)
38	5, 37	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑋 Fn 𝑃)
39		fvelrnb 6945	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
40	38, 39	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
41	36, 40	bitrd 282	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
42	35	eleq2d 2847	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ 𝑦 ∈ ran 𝑋))
43		fvelrnb 6945	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
44	38, 43	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
45	42, 44	bitrd 282	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
46	41, 45	anbi12d 644	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) ↔ (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦)))
47		fveqeq2 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦)))
48		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑥 = 𝑦 ↔ 𝑎 = 𝑦))
49	47, 48	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦)))
50		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑏 → ((𝐺 ∘ 𝐹)‘𝑦) = ((𝐺 ∘ 𝐹)‘𝑏))
51	50	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏)))
52		equequ2 2059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑏))
53	51, 52	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑏 → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
54	49, 53	rspc2v 3587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
55	54	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
56	1, 2, 3, 4, 10, 11	fcoresf1lem 48137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
57	56	adantrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
58	1, 2, 3, 4, 10, 11	fcoresf1lem 48137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
59	58	adantrl 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
60	57, 59	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) ↔ (𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏))))
61	60	imbi1d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏)))
62		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → (𝑋‘𝑎) = (𝑋‘𝑏))
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (𝑎 = 𝑏 → (𝑋‘𝑎) = (𝑋‘𝑏)))
64	63	imim2d 58	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
65	61, 64	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
66	55, 65	syld 48	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
67	66	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
68	67	com23 87	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
69	68	adantld 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
70	9, 69	biimtrid 245	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
71	8, 70	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
72	71	impl 461	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))
73		fveq2 6885	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑎) = 𝑥 → (𝑌‘(𝑋‘𝑎)) = (𝑌‘𝑥))
74		fveq2 6885	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑏) = 𝑦 → (𝑌‘(𝑋‘𝑏)) = (𝑌‘𝑦))
75	73, 74	eqeqan12rd 2776	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) ↔ (𝑌‘𝑥) = (𝑌‘𝑦)))
76		eqeq12 2778	. . . . . . . . . . . . 13 ⊢ (((𝑋‘𝑎) = 𝑥 ∧ (𝑋‘𝑏) = 𝑦) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
77	76	ancoms 464	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
78	75, 77	imbi12d 347	. . . . . . . . . . 11 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)) ↔ ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
79	72, 78	syl5ibcom 248	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
80	79	expd 421	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
81	80	rexlimdva 3164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
82	81	com23 87	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
83	82	rexlimdva 3164	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
84	83	impd 416	. . . . 5 ⊢ (𝜑 → ((∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
85	46, 84	sylbid 243	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
86	85	ralrimivv 3204	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))
87		dff13 7258	. . 3 ⊢ (𝑌:𝐸–1-1→𝐷 ↔ (𝑌:𝐸⟶𝐷 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
88	33, 86, 87	sylanbrc 595	. 2 ⊢ (𝜑 → 𝑌:𝐸–1-1→𝐷)
89	27, 88	jca 521	1 ⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087   ∩ cin 3898  ^◡ccnv 5650  ran crn 5652   ↾ cres 5653   “ cima 5654   ∘ ccom 5655   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –onto→wfo 6536  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-fv 6546

This theorem is used by:  fcoresf1b  48139  f1cof1b  48146