This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fcoresf1

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)

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

Proof

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