Theorem fcoresf1 44563

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 44559	. . . 4 ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸)
6		fof 6688	. . . 4 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋:𝑃⟶𝐸)
7	5, 6	syl 17	. . 3 ⊢ (𝜑 → 𝑋:𝑃⟶𝐸)
8		fcoresf1.i	. . . 4 ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷)
9		dff13 7128	. . . . 5 ⊢ ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ ((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)))
10		fcores.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
11		fcores.y	. . . . . . . . . . . 12 ⊢ 𝑌 = (𝐺 ↾ 𝐸)
12	1, 2, 3, 4, 10, 11	fcoresf1lem 44562	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
13	12	adantrr 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
14	1, 2, 3, 4, 10, 11	fcoresf1lem 44562	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
15	14	adantrl 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
16	13, 15	eqeq12d 2754	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
17	16	imbi1d 342	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ ((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦)))
18		fveq2 6774	. . . . . . . . . 10 ⊢ ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)))
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
20	19	imim1d 82	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
21	17, 20	sylbid 239	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
22	21	ralimdvva 3126	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
23	22	adantld 491	. . . . 5 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
24	9, 23	syl5bi 241	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
25	8, 24	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦))
26		dff13 7128	. . 3 ⊢ (𝑋:𝑃–1-1→𝐸 ↔ (𝑋:𝑃⟶𝐸 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
27	7, 25, 26	sylanbrc 583	. 2 ⊢ (𝜑 → 𝑋:𝑃–1-1→𝐸)
28	2	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐶))
29		inss2 4163	. . . . . 6 ⊢ (ran 𝐹 ∩ 𝐶) ⊆ 𝐶
30	28, 29	eqsstrdi 3975	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ 𝐶)
31	10, 30	fssresd 6641	. . . 4 ⊢ (𝜑 → (𝐺 ↾ 𝐸):𝐸⟶𝐷)
32	11	feq1i 6591	. . . 4 ⊢ (𝑌:𝐸⟶𝐷 ↔ (𝐺 ↾ 𝐸):𝐸⟶𝐷)
33	31, 32	sylibr 233	. . 3 ⊢ (𝜑 → 𝑌:𝐸⟶𝐷)
34	1, 2, 3, 4	fcoreslem2 44558	. . . . . . . . 9 ⊢ (𝜑 → ran 𝑋 = 𝐸)
35	34	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = ran 𝑋)
36	35	eleq2d 2824	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ 𝑥 ∈ ran 𝑋))
37		fofn 6690	. . . . . . . . 9 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋 Fn 𝑃)
38	5, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋 Fn 𝑃)
39		fvelrnb 6830	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
41	36, 40	bitrd 278	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
42	35	eleq2d 2824	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ 𝑦 ∈ ran 𝑋))
43		fvelrnb 6830	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
44	38, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
45	42, 44	bitrd 278	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
46	41, 45	anbi12d 631	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) ↔ (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦)))
47		fveqeq2 6783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦)))
48		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑥 = 𝑦 ↔ 𝑎 = 𝑦))
49	47, 48	imbi12d 345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦)))
50		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑏 → ((𝐺 ∘ 𝐹)‘𝑦) = ((𝐺 ∘ 𝐹)‘𝑏))
51	50	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏)))
52		equequ2 2029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑏))
53	51, 52	imbi12d 345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑏 → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
54	49, 53	rspc2v 3570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
55	54	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
56	1, 2, 3, 4, 10, 11	fcoresf1lem 44562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
57	56	adantrr 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
58	1, 2, 3, 4, 10, 11	fcoresf1lem 44562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
59	58	adantrl 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
60	57, 59	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) ↔ (𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏))))
61	60	imbi1d 342	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏)))
62		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 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	syl5bi 241	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
71	8, 70	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
72	71	impl 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))
73		fveq2 6774	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑎) = 𝑥 → (𝑌‘(𝑋‘𝑎)) = (𝑌‘𝑥))
74		fveq2 6774	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑏) = 𝑦 → (𝑌‘(𝑋‘𝑏)) = (𝑌‘𝑦))
75	73, 74	eqeqan12rd 2753	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) ↔ (𝑌‘𝑥) = (𝑌‘𝑦)))
76		eqeq12 2755	. . . . . . . . . . . . 13 ⊢ (((𝑋‘𝑎) = 𝑥 ∧ (𝑋‘𝑏) = 𝑦) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
77	76	ancoms 459	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
78	75, 77	imbi12d 345	. . . . . . . . . . 11 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)) ↔ ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
79	72, 78	syl5ibcom 244	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
80	79	expd 416	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
81	80	rexlimdva 3213	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
82	81	com23 86	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
83	82	rexlimdva 3213	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
84	83	impd 411	. . . . 5 ⊢ (𝜑 → ((∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
85	46, 84	sylbid 239	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
86	85	ralrimivv 3122	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))
87		dff13 7128	. . 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 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065   ∩ cin 3886  ^◡ccnv 5588  ran crn 5590   ↾ cres 5591   “ cima 5592   ∘ ccom 5593   Fn wfn 6428  ⟶wf 6429  –1-1→wf1 6430  –onto→wfo 6431  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-fv 6441

This theorem is referenced by:  fcoresf1b  44564  f1cof1b  44569