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 6749

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 6748	. 2 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):(^◡𝐺 “ 𝐵)–1-1→𝐶)
2		f1f 6738	. . . . . 6 ⊢ (𝐺:𝐴–1-1→𝐵 → 𝐺:𝐴⟶𝐵)
3		fimacnv 6692	. . . . . 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 6734	. . 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 5630 “ cima 5634 ∘ ccom 5635 ⟶wf 6495 –1-1→wf1 6496

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 5246 ax-nul 5256 ax-pr 5382

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 3403 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-br 5103 df-opab 5165 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504

This theorem is referenced by: f1oco 6805 f1cofveqaeqALT 7215 tposf12 8207 domtr 8955 domtrfil 9133 dfac12lem2 10074 fin23lem28 10269 pwfseqlem5 10592 cofth 17875 injsubmefmnd 18800 gsumzf1o 19818 cycpmconjv 33072 erdsze2lem2 35164 fcoresf1b 47044 fundcmpsurinjpreimafv 47382

W3C validator