Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem fac0 4871

Description: The factorial of 0.

**Assertion**
Ref	Expression
fac0	⊢ (! ‘0) = 1

**Proof of Theorem fac0**
Step	Hyp	Ref	Expression
1		df-fac 4869	. . . . 5 ⊢ ! = (( · seq(I ↾ ℕ)) ∪ {⟨0, 1⟩})
2		reseq1 2575	. . . . 5 ⊢ (! = (( · seq(I ↾ ℕ)) ∪ {⟨0, 1⟩}) → (! ↾ {0}) = ((( · seq(I ↾ ℕ)) ∪ {⟨0, 1⟩}) ↾ {0}))
3	1, 2	ax-mp 6	. . . 4 ⊢ (! ↾ {0}) = ((( · seq(I ↾ ℕ)) ∪ {⟨0, 1⟩}) ↾ {0})
4		resundir 2583	. . . 4 ⊢ ((( · seq(I ↾ ℕ)) ∪ {⟨0, 1⟩}) ↾ {0}) = ((( · seq(I ↾ ℕ)) ↾ {0}) ∪ ({⟨0, 1⟩} ↾ {0}))
5		0nnn 4443	. . . . . . . 8 ⊢ ¬ 0 ∈ ℕ
6		disjsn 1836	. . . . . . . 8 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
7	5, 6	mpbir 165	. . . . . . 7 ⊢ (ℕ ∩ {0}) = ∅
8		axmulex 4060	. . . . . . . . 9 ⊢ · ∈ V
9		nnex 4431	. . . . . . . . . 10 ⊢ ℕ ∈ V
10		funi 2692	. . . . . . . . . 10 ⊢ Fun I
11		resfunexg 2717	. . . . . . . . . 10 ⊢ (ℕ ∈ V → (Fun I → (I ↾ ℕ) ∈ V))
12	9, 10, 11	mp2 43	. . . . . . . . 9 ⊢ (I ↾ ℕ) ∈ V
13	8, 12	seqfn 4672	. . . . . . . 8 ⊢ ( · seq(I ↾ ℕ)) Fn ℕ
14		fnresdisj 2732	. . . . . . . 8 ⊢ (( · seq(I ↾ ℕ)) Fn ℕ → ((ℕ ∩ {0}) = ∅ ↔ (( · seq(I ↾ ℕ)) ↾ {0}) = ∅))
15	13, 14	ax-mp 6	. . . . . . 7 ⊢ ((ℕ ∩ {0}) = ∅ ↔ (( · seq(I ↾ ℕ)) ↾ {0}) = ∅)
16	7, 15	mpbi 164	. . . . . 6 ⊢ (( · seq(I ↾ ℕ)) ↾ {0}) = ∅
17		0nn0 4546	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
18	17	elisseti 1355	. . . . . . . 8 ⊢ 0 ∈ V
19	18	relsn 2485	. . . . . . 7 ⊢ Rel {⟨0, 1⟩}
20		dmsnop 2547	. . . . . . . 8 ⊢ dom {⟨0, 1⟩} = {0}
21		ssid 1519	. . . . . . . 8 ⊢ {0} ⊆ {0}
22	20, 21	eqsstr 1530	. . . . . . 7 ⊢ dom {⟨0, 1⟩} ⊆ {0}
23		relssres 2596	. . . . . . 7 ⊢ ((Rel {⟨0, 1⟩} ∧ dom {⟨0, 1⟩} ⊆ {0}) → ({⟨0, 1⟩} ↾ {0}) = {⟨0, 1⟩})
24	19, 22, 23	mp2an 520	. . . . . 6 ⊢ ({⟨0, 1⟩} ↾ {0}) = {⟨0, 1⟩}
25	16, 24	uneq12i 1609	. . . . 5 ⊢ ((( · seq(I ↾ ℕ)) ↾ {0}) ∪ ({⟨0, 1⟩} ↾ {0})) = (∅ ∪ {⟨0, 1⟩})
26		uncom 1604	. . . . 5 ⊢ (∅ ∪ {⟨0, 1⟩}) = ({⟨0, 1⟩} ∪ ∅)
27		un0 1721	. . . . 5 ⊢ ({⟨0, 1⟩} ∪ ∅) = {⟨0, 1⟩}
28	25, 26, 27	3eqtr 1123	. . . 4 ⊢ ((( · seq(I ↾ ℕ)) ↾ {0}) ∪ ({⟨0, 1⟩} ↾ {0})) = {⟨0, 1⟩}
29	3, 4, 28	3eqtr 1123	. . 3 ⊢ (! ↾ {0}) = {⟨0, 1⟩}
30	29	fveq1i 2833	. 2 ⊢ ((! ↾ {0}) ‘0) = ({⟨0, 1⟩} ‘0)
31	18	snid 1830	. . 3 ⊢ 0 ∈ {0}
32		fvres 2840	. . 3 ⊢ (0 ∈ {0} → ((! ↾ {0}) ‘0) = (! ‘0))
33	31, 32	ax-mp 6	. 2 ⊢ ((! ↾ {0}) ‘0) = (! ‘0)
34		1nn0 4547	. . . 4 ⊢ 1 ∈ ℕ₀
35	34	elisseti 1355	. . 3 ⊢ 1 ∈ V
36	18, 35	fvsn 2879	. 2 ⊢ ({⟨0, 1⟩} ‘0) = 1
37	30, 33, 36	3eqtr3 1124	1 ⊢ (! ‘0) = 1

Colors of variables: wff set class

Syntax hints: ¬ wn 1 ↔ wb 127 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ∪ cun 1485 ∩ cin 1486 ⊆ wss 1487 ∅c0 1707 {csn 1808 ⟨cop 1810 Icid 2057 dom cdm 2410 ↾ cres 2412 Rel wrel 2415 Fun wfun 2416 Fn wfn 2417 ‘cfv 2422 (class class class)co 3001 0cc0 4028 1c1 4029 · cmulc 4032 ℕcn 4093 ℕ₀cn0 4094 seqcseq 4660 !cfa 4868

This theorem is referenced by: facp1t 4873 facclt 4874

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-le 4277 df-n 4423 df-n0 4535 df-seq 4661 df-fac 4869

metamath.org