f1co - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1co		Structured version Visualization version GIF version

Theorem f1co 6770

Description: Composition of one-to-one functions when the codomain of the first matches the domain of the second. Exercise 30 of [TakeutiZaring] p. 25. (Contributed by NM, 28-May-1998.) (Proof shortened by AV, 20-Sep-2024.)

**Assertion**
Ref	Expression
f1co	⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1→𝐶)

**Proof of Theorem f1co**
Step	Hyp	Ref	Expression
1		f1cof1 6769	. 2 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):(^◡𝐺 “ 𝐵)–1-1→𝐶)
2		f1f 6759	. . . . . 6 ⊢ (𝐺:𝐴–1-1→𝐵 → 𝐺:𝐴⟶𝐵)
3		fimacnv 6713	. . . . . 6 ⊢ (𝐺:𝐴⟶𝐵 → (^◡𝐺 “ 𝐵) = 𝐴)
4	2, 3	syl 17	. . . . 5 ⊢ (𝐺:𝐴–1-1→𝐵 → (^◡𝐺 “ 𝐵) = 𝐴)
5	4	adantl 481	. . . 4 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (^◡𝐺 “ 𝐵) = 𝐴)
6	5	eqcomd 2736	. . 3 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → 𝐴 = (^◡𝐺 “ 𝐵))
7		f1eq2 6755	. . 3 ⊢ (𝐴 = (^◡𝐺 “ 𝐵) → ((𝐹 ∘ 𝐺):𝐴–1-1→𝐶 ↔ (𝐹 ∘ 𝐺):(^◡𝐺 “ 𝐵)–1-1→𝐶))
8	6, 7	syl 17	. 2 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → ((𝐹 ∘ 𝐺):𝐴–1-1→𝐶 ↔ (𝐹 ∘ 𝐺):(^◡𝐺 “ 𝐵)–1-1→𝐶))
9	1, 8	mpbird 257	1 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1→𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ^◡ccnv 5640 “ cima 5644 ∘ ccom 5645 ⟶wf 6510 –1-1→wf1 6511

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pr 5390

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-sn 4593 df-pr 4595 df-op 4599 df-br 5111 df-opab 5173 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519

This theorem is referenced by: f1oco 6826 f1cofveqaeqALT 7236 tposf12 8233 domtr 8981 domtrfil 9162 dfac12lem2 10105 fin23lem28 10300 pwfseqlem5 10623 cofth 17906 injsubmefmnd 18831 gsumzf1o 19849 cycpmconjv 33106 erdsze2lem2 35198 fcoresf1b 47075 fundcmpsurinjpreimafv 47413

W3C validator