Theorem fcoresf1 45293

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 45289	. . . 4 ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸)
6		fof 6756	. . . 4 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋:𝑃⟶𝐸)
7	5, 6	syl 17	. . 3 ⊢ (𝜑 → 𝑋:𝑃⟶𝐸)
8		fcoresf1.i	. . . 4 ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷)
9		dff13 7202	. . . . 5 ⊢ ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ ((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)))
10		fcores.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
11		fcores.y	. . . . . . . . . . . 12 ⊢ 𝑌 = (𝐺 ↾ 𝐸)
12	1, 2, 3, 4, 10, 11	fcoresf1lem 45292	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
13	12	adantrr 715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
14	1, 2, 3, 4, 10, 11	fcoresf1lem 45292	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
15	14	adantrl 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
16	13, 15	eqeq12d 2752	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
17	16	imbi1d 341	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ ((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦)))
18		fveq2 6842	. . . . . . . . . 10 ⊢ ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)))
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
20	19	imim1d 82	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
21	17, 20	sylbid 239	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
22	21	ralimdvva 3201	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
23	22	adantld 491	. . . . 5 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
24	9, 23	biimtrid 241	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
25	8, 24	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦))
26		dff13 7202	. . 3 ⊢ (𝑋:𝑃–1-1→𝐸 ↔ (𝑋:𝑃⟶𝐸 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
27	7, 25, 26	sylanbrc 583	. 2 ⊢ (𝜑 → 𝑋:𝑃–1-1→𝐸)
28	2	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐶))
29		inss2 4189	. . . . . 6 ⊢ (ran 𝐹 ∩ 𝐶) ⊆ 𝐶
30	28, 29	eqsstrdi 3998	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ 𝐶)
31	10, 30	fssresd 6709	. . . 4 ⊢ (𝜑 → (𝐺 ↾ 𝐸):𝐸⟶𝐷)
32	11	feq1i 6659	. . . 4 ⊢ (𝑌:𝐸⟶𝐷 ↔ (𝐺 ↾ 𝐸):𝐸⟶𝐷)
33	31, 32	sylibr 233	. . 3 ⊢ (𝜑 → 𝑌:𝐸⟶𝐷)
34	1, 2, 3, 4	fcoreslem2 45288	. . . . . . . . 9 ⊢ (𝜑 → ran 𝑋 = 𝐸)
35	34	eqcomd 2742	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = ran 𝑋)
36	35	eleq2d 2823	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ 𝑥 ∈ ran 𝑋))
37		fofn 6758	. . . . . . . . 9 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋 Fn 𝑃)
38	5, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋 Fn 𝑃)
39		fvelrnb 6903	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
41	36, 40	bitrd 278	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
42	35	eleq2d 2823	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ 𝑦 ∈ ran 𝑋))
43		fvelrnb 6903	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
44	38, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
45	42, 44	bitrd 278	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
46	41, 45	anbi12d 631	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) ↔ (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦)))
47		fveqeq2 6851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦)))
48		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑥 = 𝑦 ↔ 𝑎 = 𝑦))
49	47, 48	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦)))
50		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑏 → ((𝐺 ∘ 𝐹)‘𝑦) = ((𝐺 ∘ 𝐹)‘𝑏))
51	50	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏)))
52		equequ2 2029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑏))
53	51, 52	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑏 → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
54	49, 53	rspc2v 3590	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
55	54	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
56	1, 2, 3, 4, 10, 11	fcoresf1lem 45292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
57	56	adantrr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
58	1, 2, 3, 4, 10, 11	fcoresf1lem 45292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
59	58	adantrl 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
60	57, 59	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) ↔ (𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏))))
61	60	imbi1d 341	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏)))
62		fveq2 6842	. . . . . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
68	67	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
69	68	adantld 491	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
70	9, 69	biimtrid 241	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
71	8, 70	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
72	71	impl 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))
73		fveq2 6842	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑎) = 𝑥 → (𝑌‘(𝑋‘𝑎)) = (𝑌‘𝑥))
74		fveq2 6842	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑏) = 𝑦 → (𝑌‘(𝑋‘𝑏)) = (𝑌‘𝑦))
75	73, 74	eqeqan12rd 2751	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) ↔ (𝑌‘𝑥) = (𝑌‘𝑦)))
76		eqeq12 2753	. . . . . . . . . . . . 13 ⊢ (((𝑋‘𝑎) = 𝑥 ∧ (𝑋‘𝑏) = 𝑦) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
77	76	ancoms 459	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
78	75, 77	imbi12d 344	. . . . . . . . . . 11 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)) ↔ ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
79	72, 78	syl5ibcom 244	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
80	79	expd 416	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
81	80	rexlimdva 3152	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
82	81	com23 86	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
83	82	rexlimdva 3152	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
84	83	impd 411	. . . . 5 ⊢ (𝜑 → ((∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
85	46, 84	sylbid 239	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
86	85	ralrimivv 3195	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))
87		dff13 7202	. . 3 ⊢ (𝑌:𝐸–1-1→𝐷 ↔ (𝑌:𝐸⟶𝐷 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
88	33, 86, 87	sylanbrc 583	. 2 ⊢ (𝜑 → 𝑌:𝐸–1-1→𝐷)
89	27, 88	jca 512	1 ⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3064  ∃wrex 3073   ∩ cin 3909  ^◡ccnv 5632  ran crn 5634   ↾ cres 5635   “ cima 5636   ∘ ccom 5637   Fn wfn 6491  ⟶wf 6492  –1-1→wf1 6493  –onto→wfo 6494  ‘cfv 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-fv 6504

This theorem is referenced by:  fcoresf1b  45294  f1cof1b  45299