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 6767

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 6766	. 2 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):(^◡𝐺 “ 𝐵)–1-1→𝐶)
2		f1f 6756	. . . . . 6 ⊢ (𝐺:𝐴–1-1→𝐵 → 𝐺:𝐴⟶𝐵)
3		fimacnv 6710	. . . . . 6 ⊢ (𝐺:𝐴⟶𝐵 → (^◡𝐺 “ 𝐵) = 𝐴)
4	2, 3	syl 17	. . . . 5 ⊢ (𝐺:𝐴–1-1→𝐵 → (^◡𝐺 “ 𝐵) = 𝐴)
5	4	adantl 481	. . . 4 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (^◡𝐺 “ 𝐵) = 𝐴)
6	5	eqcomd 2735	. . 3 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → 𝐴 = (^◡𝐺 “ 𝐵))
7		f1eq2 6752	. . 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 5637 “ cima 5641 ∘ ccom 5642 ⟶wf 6507 –1-1→wf1 6508

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 2701 ax-sep 5251 ax-nul 5261 ax-pr 5387

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ral 3045 df-rex 3054 df-rab 3406 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-br 5108 df-opab 5170 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516

This theorem is referenced by: f1oco 6823 f1cofveqaeqALT 7233 tposf12 8230 domtr 8978 domtrfil 9156 dfac12lem2 10098 fin23lem28 10293 pwfseqlem5 10616 cofth 17899 injsubmefmnd 18824 gsumzf1o 19842 cycpmconjv 33099 erdsze2lem2 35191 fcoresf1b 47071 fundcmpsurinjpreimafv 47409

W3C validator