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 6251

Description: Composition of one-to-one functions. Exercise 30 of [TakeutiZaring] p. 25. (Contributed by NM, 28-May-1998.)

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

**Proof of Theorem f1co**
Step	Hyp	Ref	Expression
1		df-f1 6036	. . 3 ⊢ (𝐹:𝐵–1-1→𝐶 ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ^◡𝐹))
2		df-f1 6036	. . 3 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
3		fco 6198	. . . . 5 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
4		funco 6071	. . . . . . 7 ⊢ ((Fun ^◡𝐺 ∧ Fun ^◡𝐹) → Fun (^◡𝐺 ∘ ^◡𝐹))
5		cnvco 5446	. . . . . . . 8 ⊢ ^◡(𝐹 ∘ 𝐺) = (^◡𝐺 ∘ ^◡𝐹)
6	5	funeqi 6052	. . . . . . 7 ⊢ (Fun ^◡(𝐹 ∘ 𝐺) ↔ Fun (^◡𝐺 ∘ ^◡𝐹))
7	4, 6	sylibr 224	. . . . . 6 ⊢ ((Fun ^◡𝐺 ∧ Fun ^◡𝐹) → Fun ^◡(𝐹 ∘ 𝐺))
8	7	ancoms 455	. . . . 5 ⊢ ((Fun ^◡𝐹 ∧ Fun ^◡𝐺) → Fun ^◡(𝐹 ∘ 𝐺))
9	3, 8	anim12i 592	. . . 4 ⊢ (((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) ∧ (Fun ^◡𝐹 ∧ Fun ^◡𝐺)) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ∧ Fun ^◡(𝐹 ∘ 𝐺)))
10	9	an4s 631	. . 3 ⊢ (((𝐹:𝐵⟶𝐶 ∧ Fun ^◡𝐹) ∧ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ∧ Fun ^◡(𝐹 ∘ 𝐺)))
11	1, 2, 10	syl2anb 577	. 2 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ∧ Fun ^◡(𝐹 ∘ 𝐺)))
12		df-f1 6036	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴–1-1→𝐶 ↔ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ∧ Fun ^◡(𝐹 ∘ 𝐺)))
13	11, 12	sylibr 224	1 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1→𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 382 ^◡ccnv 5248 ∘ ccom 5253 Fun wfun 6025 ⟶wf 6027 –1-1→wf1 6028

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-sep 4912 ax-nul 4920 ax-pr 5034

This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-eu 2621 df-mo 2622 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ral 3065 df-rex 3066 df-rab 3069 df-v 3351 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-sn 4315 df-pr 4317 df-op 4321 df-br 4785 df-opab 4845 df-id 5157 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036

This theorem is referenced by: f1oco 6300 f1cofveqaeqALT 6658 tposf12 7528 domtr 8161 dfac12lem2 9167 fin23lem28 9363 pwfseqlem5 9686 cofth 16801 gsumzf1o 18519 erdsze2lem2 31518