Theorem fcoresf1 44178

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 44174	. . . 4 ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸)
6		fof 6611	. . . 4 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋:𝑃⟶𝐸)
7	5, 6	syl 17	. . 3 ⊢ (𝜑 → 𝑋:𝑃⟶𝐸)
8		fcoresf1.i	. . . 4 ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷)
9		dff13 7045	. . . . 5 ⊢ ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ ((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)))
10		fcores.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
11		fcores.y	. . . . . . . . . . . 12 ⊢ 𝑌 = (𝐺 ↾ 𝐸)
12	1, 2, 3, 4, 10, 11	fcoresf1lem 44177	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
13	12	adantrr 717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝑌‘(𝑋‘𝑥)))
14	1, 2, 3, 4, 10, 11	fcoresf1lem 44177	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
15	14	adantrl 716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝑌‘(𝑋‘𝑦)))
16	13, 15	eqeq12d 2752	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
17	16	imbi1d 345	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ ((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦)))
18		fveq2 6695	. . . . . . . . . 10 ⊢ ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)))
19	18	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((𝑋‘𝑥) = (𝑋‘𝑦) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦))))
20	19	imim1d 82	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝑋‘𝑦)) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
21	17, 20	sylbid 243	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
22	21	ralimdvva 3092	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
23	22	adantld 494	. . . . 5 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
24	9, 23	syl5bi 245	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
25	8, 24	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦))
26		dff13 7045	. . 3 ⊢ (𝑋:𝑃–1-1→𝐸 ↔ (𝑋:𝑃⟶𝐸 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ((𝑋‘𝑥) = (𝑋‘𝑦) → 𝑥 = 𝑦)))
27	7, 25, 26	sylanbrc 586	. 2 ⊢ (𝜑 → 𝑋:𝑃–1-1→𝐸)
28	2	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐶))
29		inss2 4130	. . . . . 6 ⊢ (ran 𝐹 ∩ 𝐶) ⊆ 𝐶
30	28, 29	eqsstrdi 3941	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ 𝐶)
31	10, 30	fssresd 6564	. . . 4 ⊢ (𝜑 → (𝐺 ↾ 𝐸):𝐸⟶𝐷)
32	11	feq1i 6514	. . . 4 ⊢ (𝑌:𝐸⟶𝐷 ↔ (𝐺 ↾ 𝐸):𝐸⟶𝐷)
33	31, 32	sylibr 237	. . 3 ⊢ (𝜑 → 𝑌:𝐸⟶𝐷)
34	1, 2, 3, 4	fcoreslem2 44173	. . . . . . . . 9 ⊢ (𝜑 → ran 𝑋 = 𝐸)
35	34	eqcomd 2742	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = ran 𝑋)
36	35	eleq2d 2816	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ 𝑥 ∈ ran 𝑋))
37		fofn 6613	. . . . . . . . 9 ⊢ (𝑋:𝑃–onto→𝐸 → 𝑋 Fn 𝑃)
38	5, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋 Fn 𝑃)
39		fvelrnb 6751	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
41	36, 40	bitrd 282	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐸 ↔ ∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥))
42	35	eleq2d 2816	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ 𝑦 ∈ ran 𝑋))
43		fvelrnb 6751	. . . . . . . 8 ⊢ (𝑋 Fn 𝑃 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
44	38, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
45	42, 44	bitrd 282	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐸 ↔ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦))
46	41, 45	anbi12d 634	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) ↔ (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦)))
47		fveqeq2 6704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦)))
48		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑥 = 𝑦 ↔ 𝑎 = 𝑦))
49	47, 48	imbi12d 348	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → ((((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦)))
50		fveq2 6695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑏 → ((𝐺 ∘ 𝐹)‘𝑦) = ((𝐺 ∘ 𝐹)‘𝑏))
51	50	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) ↔ ((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏)))
52		equequ2 2036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑏))
53	51, 52	imbi12d 348	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑏 → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑎 = 𝑦) ↔ (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
54	49, 53	rspc2v 3537	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
55	54	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏)))
56	1, 2, 3, 4, 10, 11	fcoresf1lem 44177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
57	56	adantrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑎) = (𝑌‘(𝑋‘𝑎)))
58	1, 2, 3, 4, 10, 11	fcoresf1lem 44177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
59	58	adantrl 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐺 ∘ 𝐹)‘𝑏) = (𝑌‘(𝑋‘𝑏)))
60	57, 59	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) ↔ (𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏))))
61	60	imbi1d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏)))
62		fveq2 6695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → (𝑋‘𝑎) = (𝑋‘𝑏))
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (𝑎 = 𝑏 → (𝑋‘𝑎) = (𝑋‘𝑏)))
64	63	imim2d 57	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → 𝑎 = 𝑏) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
65	61, 64	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((((𝐺 ∘ 𝐹)‘𝑎) = ((𝐺 ∘ 𝐹)‘𝑏) → 𝑎 = 𝑏) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
66	55, 65	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
67	66	ex 416	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
68	67	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
69	68	adantld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃⟶𝐷 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (((𝐺 ∘ 𝐹)‘𝑥) = ((𝐺 ∘ 𝐹)‘𝑦) → 𝑥 = 𝑦)) → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
70	9, 69	syl5bi 245	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))))
71	8, 70	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏))))
72	71	impl 459	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)))
73		fveq2 6695	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑎) = 𝑥 → (𝑌‘(𝑋‘𝑎)) = (𝑌‘𝑥))
74		fveq2 6695	. . . . . . . . . . . . 13 ⊢ ((𝑋‘𝑏) = 𝑦 → (𝑌‘(𝑋‘𝑏)) = (𝑌‘𝑦))
75	73, 74	eqeqan12rd 2755	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) ↔ (𝑌‘𝑥) = (𝑌‘𝑦)))
76		eqeq12 2750	. . . . . . . . . . . . 13 ⊢ (((𝑋‘𝑎) = 𝑥 ∧ (𝑋‘𝑏) = 𝑦) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
77	76	ancoms 462	. . . . . . . . . . . 12 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑋‘𝑎) = (𝑋‘𝑏) ↔ 𝑥 = 𝑦))
78	75, 77	imbi12d 348	. . . . . . . . . . 11 ⊢ (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → (((𝑌‘(𝑋‘𝑎)) = (𝑌‘(𝑋‘𝑏)) → (𝑋‘𝑎) = (𝑋‘𝑏)) ↔ ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
79	72, 78	syl5ibcom 248	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (((𝑋‘𝑏) = 𝑦 ∧ (𝑋‘𝑎) = 𝑥) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
80	79	expd 419	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
81	80	rexlimdva 3193	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑋‘𝑎) = 𝑥 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
82	81	com23 86	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ((𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
83	82	rexlimdva 3193	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 → (∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦 → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))))
84	83	impd 414	. . . . 5 ⊢ (𝜑 → ((∃𝑎 ∈ 𝑃 (𝑋‘𝑎) = 𝑥 ∧ ∃𝑏 ∈ 𝑃 (𝑋‘𝑏) = 𝑦) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
85	46, 84	sylbid 243	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸) → ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
86	85	ralrimivv 3101	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦))
87		dff13 7045	. . 3 ⊢ (𝑌:𝐸–1-1→𝐷 ↔ (𝑌:𝐸⟶𝐷 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐸 ((𝑌‘𝑥) = (𝑌‘𝑦) → 𝑥 = 𝑦)))
88	33, 86, 87	sylanbrc 586	. 2 ⊢ (𝜑 → 𝑌:𝐸–1-1→𝐷)
89	27, 88	jca 515	1 ⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ∃wrex 3052   ∩ cin 3852  ^◡ccnv 5535  ran crn 5537   ↾ cres 5538   “ cima 5539   ∘ ccom 5540   Fn wfn 6353  ⟶wf 6354  –1-1→wf1 6355  –onto→wfo 6356  ‘cfv 6358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-fv 6366

This theorem is referenced by:  fcoresf1b  44179  f1cof1b  44184