Theorem fcoresf1 44450

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 44446	. . . 4 ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸)
6		fof 6672	. . . 4 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋:𝑃⟶𝐸)
7	5, 6	syl 17	. . 3 ⊢ (𝜑 → 𝑋:𝑃⟶𝐸)
8		fcoresf1.i	. . . 4 ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷)
9		dff13 7109	. . . . 5 ⊢ ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ ((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)))
10		fcores.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
11		fcores.y	. . . . . . . . . . . 12 ⊢ 𝑌 = (𝐺 ↾ 𝐸)
12	1, 2, 3, 4, 10, 11	fcoresf1lem 44449	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
13	12	adantrr 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
14	1, 2, 3, 4, 10, 11	fcoresf1lem 44449	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
15	14	adantrl 712	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
16	13, 15	eqeq12d 2754	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
17	16	imbi1d 341	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ ((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦)))
18		fveq2 6756	. . . . . . . . . 10 ⊢ ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)))
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
20	19	imim1d 82	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
21	17, 20	sylbid 239	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
22	21	ralimdvva 3104	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
23	22	adantld 490	. . . . 5 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
24	9, 23	syl5bi 241	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
25	8, 24	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦))
26		dff13 7109	. . 3 ⊢ (𝑋:𝑃–1-1→𝐸 ↔ (𝑋:𝑃⟶𝐸 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
27	7, 25, 26	sylanbrc 582	. 2 ⊢ (𝜑 → 𝑋:𝑃–1-1→𝐸)
28	2	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐶))
29		inss2 4160	. . . . . 6 ⊢ (ran 𝐹 ∩ 𝐶) ⊆ 𝐶
30	28, 29	eqsstrdi 3971	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ 𝐶)
31	10, 30	fssresd 6625	. . . 4 ⊢ (𝜑 → (𝐺 ↾ 𝐸):𝐸⟶𝐷)
32	11	feq1i 6575	. . . 4 ⊢ (𝑌:𝐸⟶𝐷 ↔ (𝐺 ↾ 𝐸):𝐸⟶𝐷)
33	31, 32	sylibr 233	. . 3 ⊢ (𝜑 → 𝑌:𝐸⟶𝐷)
34	1, 2, 3, 4	fcoreslem2 44445	. . . . . . . . 9 ⊢ (𝜑 → ran 𝑋 = 𝐸)
35	34	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = ran 𝑋)
36	35	eleq2d 2824	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ 𝑥 ∈ ran 𝑋))
37		fofn 6674	. . . . . . . . 9 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋 Fn 𝑃)
38	5, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋 Fn 𝑃)
39		fvelrnb 6812	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
41	36, 40	bitrd 278	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
42	35	eleq2d 2824	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ 𝑦 ∈ ran 𝑋))
43		fvelrnb 6812	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
44	38, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
45	42, 44	bitrd 278	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
46	41, 45	anbi12d 630	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) ↔ (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦)))
47		fveqeq2 6765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦)))
48		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑥 = 𝑦 ↔ 𝑎 = 𝑦))
49	47, 48	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦)))
50		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑏 → ((𝐺 ∘ 𝐹)‘𝑦) = ((𝐺 ∘ 𝐹)‘𝑏))
51	50	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏)))
52		equequ2 2030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑏))
53	51, 52	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑏 → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
54	49, 53	rspc2v 3562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
55	54	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
56	1, 2, 3, 4, 10, 11	fcoresf1lem 44449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
57	56	adantrr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
58	1, 2, 3, 4, 10, 11	fcoresf1lem 44449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
59	58	adantrl 712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
60	57, 59	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) ↔ (𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏))))
61	60	imbi1d 341	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏)))
62		fveq2 6756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → (𝑋‘𝑎) = (𝑋‘𝑏))
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (𝑎 = 𝑏 → (𝑋‘𝑎) = (𝑋‘𝑏)))
64	63	imim2d 57	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
65	61, 64	sylbid 239	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
66	55, 65	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
67	66	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
68	67	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
69	68	adantld 490	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
70	9, 69	syl5bi 241	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
71	8, 70	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
72	71	impl 455	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))
73		fveq2 6756	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑎) = 𝑥 → (𝑌‘(𝑋‘𝑎)) = (𝑌‘𝑥))
74		fveq2 6756	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑏) = 𝑦 → (𝑌‘(𝑋‘𝑏)) = (𝑌‘𝑦))
75	73, 74	eqeqan12rd 2753	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) ↔ (𝑌‘𝑥) = (𝑌‘𝑦)))
76		eqeq12 2755	. . . . . . . . . . . . 13 ⊢ (((𝑋‘𝑎) = 𝑥 ∧ (𝑋‘𝑏) = 𝑦) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
77	76	ancoms 458	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
78	75, 77	imbi12d 344	. . . . . . . . . . 11 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)) ↔ ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
79	72, 78	syl5ibcom 244	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
80	79	expd 415	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
81	80	rexlimdva 3212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
82	81	com23 86	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
83	82	rexlimdva 3212	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
84	83	impd 410	. . . . 5 ⊢ (𝜑 → ((∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
85	46, 84	sylbid 239	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
86	85	ralrimivv 3113	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))
87		dff13 7109	. . 3 ⊢ (𝑌:𝐸–1-1→𝐷 ↔ (𝑌:𝐸⟶𝐷 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
88	33, 86, 87	sylanbrc 582	. 2 ⊢ (𝜑 → 𝑌:𝐸–1-1→𝐷)
89	27, 88	jca 511	1 ⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064   ∩ cin 3882  ^◡ccnv 5579  ran crn 5581   ↾ cres 5582   “ cima 5583   ∘ ccom 5584   Fn wfn 6413  ⟶wf 6414  –1-1→wf1 6415  –onto→wfo 6416  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-fv 6426

This theorem is referenced by:  fcoresf1b  44451  f1cof1b  44456