Metamath Proof Explorer


Theorem igamf

Description: Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017)

Ref Expression
Assertion igamf 1 Γ :

Proof

Step Hyp Ref Expression
1 df-igam 1 Γ = x if x 0 1 Γ x
2 0cnd x x 0
3 eldif x x ¬ x
4 gamcl x Γ x
5 gamne0 x Γ x 0
6 4 5 reccld x 1 Γ x
7 3 6 sylbir x ¬ x 1 Γ x
8 2 7 ifclda x if x 0 1 Γ x
9 1 8 fmpti 1 Γ :