Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fcoresf1 Structured version   Visualization version   GIF version

Theorem fcoresf1 45389
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.
StepHypRef Expression
1 fcores.f . . . . 5 (𝜑𝐹:𝐴𝐵)
2 fcores.e . . . . 5 𝐸 = (ran 𝐹𝐶)
3 fcores.p . . . . 5 𝑃 = (𝐹𝐶)
4 fcores.x . . . . 5 𝑋 = (𝐹𝑃)
51, 2, 3, 4fcoreslem3 45385 . . . 4 (𝜑𝑋:𝑃onto𝐸)
6 fof 6757 . . . 4 (𝑋:𝑃onto𝐸𝑋:𝑃𝐸)
75, 6syl 17 . . 3 (𝜑𝑋:𝑃𝐸)
8 fcoresf1.i . . . 4 (𝜑 → (𝐺𝐹):𝑃1-1𝐷)
9 dff13 7203 . . . . 5 ((𝐺𝐹):𝑃1-1𝐷 ↔ ((𝐺𝐹):𝑃𝐷 ∧ ∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦)))
10 fcores.g . . . . . . . . . . . 12 (𝜑𝐺:𝐶𝐷)
11 fcores.y . . . . . . . . . . . 12 𝑌 = (𝐺𝐸)
121, 2, 3, 4, 10, 11fcoresf1lem 45388 . . . . . . . . . . 11 ((𝜑𝑥𝑃) → ((𝐺𝐹)‘𝑥) = (𝑌‘(𝑋𝑥)))
1312adantrr 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑃𝑦𝑃)) → ((𝐺𝐹)‘𝑥) = (𝑌‘(𝑋𝑥)))
141, 2, 3, 4, 10, 11fcoresf1lem 45388 . . . . . . . . . . 11 ((𝜑𝑦𝑃) → ((𝐺𝐹)‘𝑦) = (𝑌‘(𝑋𝑦)))
1514adantrl 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑃𝑦𝑃)) → ((𝐺𝐹)‘𝑦) = (𝑌‘(𝑋𝑦)))
1613, 15eqeq12d 2749 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑃𝑦𝑃)) → (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) ↔ (𝑌‘(𝑋𝑥)) = (𝑌‘(𝑋𝑦))))
1716imbi1d 342 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃𝑦𝑃)) → ((((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ ((𝑌‘(𝑋𝑥)) = (𝑌‘(𝑋𝑦)) → 𝑥 = 𝑦)))
18 fveq2 6843 . . . . . . . . . 10 ((𝑋𝑥) = (𝑋𝑦) → (𝑌‘(𝑋𝑥)) = (𝑌‘(𝑋𝑦)))
1918a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑃𝑦𝑃)) → ((𝑋𝑥) = (𝑋𝑦) → (𝑌‘(𝑋𝑥)) = (𝑌‘(𝑋𝑦))))
2019imim1d 82 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃𝑦𝑃)) → (((𝑌‘(𝑋𝑥)) = (𝑌‘(𝑋𝑦)) → 𝑥 = 𝑦) → ((𝑋𝑥) = (𝑋𝑦) → 𝑥 = 𝑦)))
2117, 20sylbid 239 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃𝑦𝑃)) → ((((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑋𝑥) = (𝑋𝑦) → 𝑥 = 𝑦)))
2221ralimdvva 3198 . . . . . 6 (𝜑 → (∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) → ∀𝑥𝑃𝑦𝑃 ((𝑋𝑥) = (𝑋𝑦) → 𝑥 = 𝑦)))
2322adantld 492 . . . . 5 (𝜑 → (((𝐺𝐹):𝑃𝐷 ∧ ∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦)) → ∀𝑥𝑃𝑦𝑃 ((𝑋𝑥) = (𝑋𝑦) → 𝑥 = 𝑦)))
249, 23biimtrid 241 . . . 4 (𝜑 → ((𝐺𝐹):𝑃1-1𝐷 → ∀𝑥𝑃𝑦𝑃 ((𝑋𝑥) = (𝑋𝑦) → 𝑥 = 𝑦)))
258, 24mpd 15 . . 3 (𝜑 → ∀𝑥𝑃𝑦𝑃 ((𝑋𝑥) = (𝑋𝑦) → 𝑥 = 𝑦))
26 dff13 7203 . . 3 (𝑋:𝑃1-1𝐸 ↔ (𝑋:𝑃𝐸 ∧ ∀𝑥𝑃𝑦𝑃 ((𝑋𝑥) = (𝑋𝑦) → 𝑥 = 𝑦)))
277, 25, 26sylanbrc 584 . 2 (𝜑𝑋:𝑃1-1𝐸)
282a1i 11 . . . . . 6 (𝜑𝐸 = (ran 𝐹𝐶))
29 inss2 4190 . . . . . 6 (ran 𝐹𝐶) ⊆ 𝐶
3028, 29eqsstrdi 3999 . . . . 5 (𝜑𝐸𝐶)
3110, 30fssresd 6710 . . . 4 (𝜑 → (𝐺𝐸):𝐸𝐷)
3211feq1i 6660 . . . 4 (𝑌:𝐸𝐷 ↔ (𝐺𝐸):𝐸𝐷)
3331, 32sylibr 233 . . 3 (𝜑𝑌:𝐸𝐷)
341, 2, 3, 4fcoreslem2 45384 . . . . . . . . 9 (𝜑 → ran 𝑋 = 𝐸)
3534eqcomd 2739 . . . . . . . 8 (𝜑𝐸 = ran 𝑋)
3635eleq2d 2820 . . . . . . 7 (𝜑 → (𝑥𝐸𝑥 ∈ ran 𝑋))
37 fofn 6759 . . . . . . . . 9 (𝑋:𝑃onto𝐸𝑋 Fn 𝑃)
385, 37syl 17 . . . . . . . 8 (𝜑𝑋 Fn 𝑃)
39 fvelrnb 6904 . . . . . . . 8 (𝑋 Fn 𝑃 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎𝑃 (𝑋𝑎) = 𝑥))
4038, 39syl 17 . . . . . . 7 (𝜑 → (𝑥 ∈ ran 𝑋 ↔ ∃𝑎𝑃 (𝑋𝑎) = 𝑥))
4136, 40bitrd 279 . . . . . 6 (𝜑 → (𝑥𝐸 ↔ ∃𝑎𝑃 (𝑋𝑎) = 𝑥))
4235eleq2d 2820 . . . . . . 7 (𝜑 → (𝑦𝐸𝑦 ∈ ran 𝑋))
43 fvelrnb 6904 . . . . . . . 8 (𝑋 Fn 𝑃 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏𝑃 (𝑋𝑏) = 𝑦))
4438, 43syl 17 . . . . . . 7 (𝜑 → (𝑦 ∈ ran 𝑋 ↔ ∃𝑏𝑃 (𝑋𝑏) = 𝑦))
4542, 44bitrd 279 . . . . . 6 (𝜑 → (𝑦𝐸 ↔ ∃𝑏𝑃 (𝑋𝑏) = 𝑦))
4641, 45anbi12d 632 . . . . 5 (𝜑 → ((𝑥𝐸𝑦𝐸) ↔ (∃𝑎𝑃 (𝑋𝑎) = 𝑥 ∧ ∃𝑏𝑃 (𝑋𝑏) = 𝑦)))
47 fveqeq2 6852 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑎 → (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) ↔ ((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑦)))
48 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑎 → (𝑥 = 𝑦𝑎 = 𝑦))
4947, 48imbi12d 345 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎 → ((((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑦) → 𝑎 = 𝑦)))
50 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑏 → ((𝐺𝐹)‘𝑦) = ((𝐺𝐹)‘𝑏))
5150eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑦) ↔ ((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑏)))
52 equequ2 2030 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝑎 = 𝑦𝑎 = 𝑏))
5351, 52imbi12d 345 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → ((((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑦) → 𝑎 = 𝑦) ↔ (((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑏) → 𝑎 = 𝑏)))
5449, 53rspc2v 3589 . . . . . . . . . . . . . . . . . . 19 ((𝑎𝑃𝑏𝑃) → (∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑏) → 𝑎 = 𝑏)))
5554adantl 483 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → (∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) → (((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑏) → 𝑎 = 𝑏)))
561, 2, 3, 4, 10, 11fcoresf1lem 45388 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝑃) → ((𝐺𝐹)‘𝑎) = (𝑌‘(𝑋𝑎)))
5756adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → ((𝐺𝐹)‘𝑎) = (𝑌‘(𝑋𝑎)))
581, 2, 3, 4, 10, 11fcoresf1lem 45388 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝑃) → ((𝐺𝐹)‘𝑏) = (𝑌‘(𝑋𝑏)))
5958adantrl 715 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → ((𝐺𝐹)‘𝑏) = (𝑌‘(𝑋𝑏)))
6057, 59eqeq12d 2749 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → (((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑏) ↔ (𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏))))
6160imbi1d 342 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → ((((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → 𝑎 = 𝑏)))
62 fveq2 6843 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑏 → (𝑋𝑎) = (𝑋𝑏))
6362a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → (𝑎 = 𝑏 → (𝑋𝑎) = (𝑋𝑏)))
6463imim2d 57 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → (((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → 𝑎 = 𝑏) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏))))
6561, 64sylbid 239 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → ((((𝐺𝐹)‘𝑎) = ((𝐺𝐹)‘𝑏) → 𝑎 = 𝑏) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏))))
6655, 65syld 47 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑃𝑏𝑃)) → (∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏))))
6766ex 414 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑎𝑃𝑏𝑃) → (∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏)))))
6867com23 86 . . . . . . . . . . . . . . 15 (𝜑 → (∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦) → ((𝑎𝑃𝑏𝑃) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏)))))
6968adantld 492 . . . . . . . . . . . . . 14 (𝜑 → (((𝐺𝐹):𝑃𝐷 ∧ ∀𝑥𝑃𝑦𝑃 (((𝐺𝐹)‘𝑥) = ((𝐺𝐹)‘𝑦) → 𝑥 = 𝑦)) → ((𝑎𝑃𝑏𝑃) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏)))))
709, 69biimtrid 241 . . . . . . . . . . . . 13 (𝜑 → ((𝐺𝐹):𝑃1-1𝐷 → ((𝑎𝑃𝑏𝑃) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏)))))
718, 70mpd 15 . . . . . . . . . . . 12 (𝜑 → ((𝑎𝑃𝑏𝑃) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏))))
7271impl 457 . . . . . . . . . . 11 (((𝜑𝑎𝑃) ∧ 𝑏𝑃) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏)))
73 fveq2 6843 . . . . . . . . . . . . 13 ((𝑋𝑎) = 𝑥 → (𝑌‘(𝑋𝑎)) = (𝑌𝑥))
74 fveq2 6843 . . . . . . . . . . . . 13 ((𝑋𝑏) = 𝑦 → (𝑌‘(𝑋𝑏)) = (𝑌𝑦))
7573, 74eqeqan12rd 2748 . . . . . . . . . . . 12 (((𝑋𝑏) = 𝑦 ∧ (𝑋𝑎) = 𝑥) → ((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) ↔ (𝑌𝑥) = (𝑌𝑦)))
76 eqeq12 2750 . . . . . . . . . . . . 13 (((𝑋𝑎) = 𝑥 ∧ (𝑋𝑏) = 𝑦) → ((𝑋𝑎) = (𝑋𝑏) ↔ 𝑥 = 𝑦))
7776ancoms 460 . . . . . . . . . . . 12 (((𝑋𝑏) = 𝑦 ∧ (𝑋𝑎) = 𝑥) → ((𝑋𝑎) = (𝑋𝑏) ↔ 𝑥 = 𝑦))
7875, 77imbi12d 345 . . . . . . . . . . 11 (((𝑋𝑏) = 𝑦 ∧ (𝑋𝑎) = 𝑥) → (((𝑌‘(𝑋𝑎)) = (𝑌‘(𝑋𝑏)) → (𝑋𝑎) = (𝑋𝑏)) ↔ ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦)))
7972, 78syl5ibcom 244 . . . . . . . . . 10 (((𝜑𝑎𝑃) ∧ 𝑏𝑃) → (((𝑋𝑏) = 𝑦 ∧ (𝑋𝑎) = 𝑥) → ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦)))
8079expd 417 . . . . . . . . 9 (((𝜑𝑎𝑃) ∧ 𝑏𝑃) → ((𝑋𝑏) = 𝑦 → ((𝑋𝑎) = 𝑥 → ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦))))
8180rexlimdva 3149 . . . . . . . 8 ((𝜑𝑎𝑃) → (∃𝑏𝑃 (𝑋𝑏) = 𝑦 → ((𝑋𝑎) = 𝑥 → ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦))))
8281com23 86 . . . . . . 7 ((𝜑𝑎𝑃) → ((𝑋𝑎) = 𝑥 → (∃𝑏𝑃 (𝑋𝑏) = 𝑦 → ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦))))
8382rexlimdva 3149 . . . . . 6 (𝜑 → (∃𝑎𝑃 (𝑋𝑎) = 𝑥 → (∃𝑏𝑃 (𝑋𝑏) = 𝑦 → ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦))))
8483impd 412 . . . . 5 (𝜑 → ((∃𝑎𝑃 (𝑋𝑎) = 𝑥 ∧ ∃𝑏𝑃 (𝑋𝑏) = 𝑦) → ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦)))
8546, 84sylbid 239 . . . 4 (𝜑 → ((𝑥𝐸𝑦𝐸) → ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦)))
8685ralrimivv 3192 . . 3 (𝜑 → ∀𝑥𝐸𝑦𝐸 ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦))
87 dff13 7203 . . 3 (𝑌:𝐸1-1𝐷 ↔ (𝑌:𝐸𝐷 ∧ ∀𝑥𝐸𝑦𝐸 ((𝑌𝑥) = (𝑌𝑦) → 𝑥 = 𝑦)))
8833, 86, 87sylanbrc 584 . 2 (𝜑𝑌:𝐸1-1𝐷)
8927, 88jca 513 1 (𝜑 → (𝑋:𝑃1-1𝐸𝑌:𝐸1-1𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3061  wrex 3070  cin 3910  ccnv 5633  ran crn 5635  cres 5636  cima 5637  ccom 5638   Fn wfn 6492  wf 6493  1-1wf1 6494  ontowfo 6495  cfv 6497
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-fv 6505
This theorem is referenced by:  fcoresf1b  45390  f1cof1b  45395
  Copyright terms: Public domain W3C validator