Theorem fcoresf1ob 47030

Description: A composition is bijective iff the restriction of its first component to the minimum domain is bijective and the restriction of its second component to the minimum domain is injective. (Contributed by GL and AV, 7-Oct-2024.)

Hypotheses

Ref	Expression
fcores.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fcores.e	⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)
fcores.p	⊢ 𝑃 = (◡𝐹 “ 𝐶)
fcores.x	⊢ 𝑋 = (𝐹 ↾ 𝑃)
fcores.g	⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
fcores.y	⊢ 𝑌 = (𝐺 ↾ 𝐸)

Assertion

Ref	Expression
fcoresf1ob	⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1-onto→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1-onto→𝐷)))

Proof of Theorem fcoresf1ob

Step	Hyp	Ref	Expression
1		fcores.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fcores.e	. . . . 5 ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)
3		fcores.p	. . . . 5 ⊢ 𝑃 = (◡𝐹 “ 𝐶)
4		fcores.x	. . . . 5 ⊢ 𝑋 = (𝐹 ↾ 𝑃)
5		fcores.g	. . . . 5 ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)
6		fcores.y	. . . . 5 ⊢ 𝑌 = (𝐺 ↾ 𝐸)
7	1, 2, 3, 4, 5, 6	fcoresf1b 47027	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷)))
8	1, 2, 3, 4, 5, 6	fcoresfob 47029	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–onto→𝐷 ↔ 𝑌:𝐸–onto→𝐷))
9	7, 8	anbi12d 632	. . 3 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ∧ (𝐺 ∘ 𝐹):𝑃–onto→𝐷) ↔ ((𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷) ∧ 𝑌:𝐸–onto→𝐷)))
10		anass 468	. . 3 ⊢ (((𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷) ∧ 𝑌:𝐸–onto→𝐷) ↔ (𝑋:𝑃–1-1→𝐸 ∧ (𝑌:𝐸–1-1→𝐷 ∧ 𝑌:𝐸–onto→𝐷)))
11	9, 10	bitrdi 287	. 2 ⊢ (𝜑 → (((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ∧ (𝐺 ∘ 𝐹):𝑃–onto→𝐷) ↔ (𝑋:𝑃–1-1→𝐸 ∧ (𝑌:𝐸–1-1→𝐷 ∧ 𝑌:𝐸–onto→𝐷))))
12		df-f1o 6534	. 2 ⊢ ((𝐺 ∘ 𝐹):𝑃–1-1-onto→𝐷 ↔ ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ∧ (𝐺 ∘ 𝐹):𝑃–onto→𝐷))
13		df-f1o 6534	. . 3 ⊢ (𝑌:𝐸–1-1-onto→𝐷 ↔ (𝑌:𝐸–1-1→𝐷 ∧ 𝑌:𝐸–onto→𝐷))
14	13	anbi2i 623	. 2 ⊢ ((𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1-onto→𝐷) ↔ (𝑋:𝑃–1-1→𝐸 ∧ (𝑌:𝐸–1-1→𝐷 ∧ 𝑌:𝐸–onto→𝐷)))
15	11, 12, 14	3bitr4g 314	1 ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1-onto→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1-onto→𝐷)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∩ cin 3923  ^◡ccnv 5650  ran crn 5652   ↾ cres 5653   “ cima 5654   ∘ ccom 5655  ⟶wf 6523  –1-1→wf1 6524  –onto→wfo 6525  –1-1-onto→wf1o 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535

This theorem is referenced by:  3f1oss1  47032