Theorem lamisf ≪ | index | src | ≫ 

theorem lamisf {x: nat} (a: nat x): $ isfun (\ x, a) $;
StepHypRefExpression
1 ellam 
u, v e. \ x, a <-> E. x u, v = x, a
2 nflam1 
FS/ x \ x, a
3 2 nfel2 
F/ x u, w e. \ x, a
4 nfv 
F/ x v = w
5 3, 4 nfim 
F/ x u, w e. \ x, a -> v = w
6 prth 
u, v = x, a <-> u = x /\ v = a
7 bitr 
(u, w e. \ x, a <-> E. x u, w = x, a) -> (E. x u, w = x, a <-> E. y u, w = y, N[y / x] a) -> (u, w e. \ x, a <-> E. y u, w = y, N[y / x] a)
8 ellam 
u, w e. \ x, a <-> E. x u, w = x, a
9 7, 8 ax_mp 
(E. x u, w = x, a <-> E. y u, w = y, N[y / x] a) -> (u, w e. \ x, a <-> E. y u, w = y, N[y / x] a)
10 nfv 
F/ y u, w = x, a
11 nfnv 
FN/ x y
12 nfsbn1 
FN/ x N[y / x] a
13 11, 12 nfpr 
FN/ x y, N[y / x] a
14 13 nfeq2 
F/ x u, w = y, N[y / x] a
15 id 
x = y -> x = y
16 sbnq 
x = y -> a = N[y / x] a
17 15, 16 preqd 
x = y -> x, a = y, N[y / x] a
18 17 eqeq2d 
x = y -> (u, w = x, a <-> u, w = y, N[y / x] a)
19 10, 14, 18 cbvexh 
E. x u, w = x, a <-> E. y u, w = y, N[y / x] a
20 9, 19 ax_mp 
u, w e. \ x, a <-> E. y u, w = y, N[y / x] a
21 prth 
u, w = y, N[y / x] a <-> u = y /\ w = N[y / x] a
22 anlr 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> v = a
23 anrr 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> w = N[y / x] a
24 anll 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> u = x
25 anrl 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> u = y
26 24, 25 eqtr3d 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> x = y
27 16, 26 syl 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> a = N[y / x] a
28 23, 27 eqtr4d 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> w = a
29 22, 28 eqtr4d 
u = x /\ v = a /\ (u = y /\ w = N[y / x] a) -> v = w
30 29 exp 
u = x /\ v = a -> u = y /\ w = N[y / x] a -> v = w
31 21, 30 syl5bi 
u = x /\ v = a -> u, w = y, N[y / x] a -> v = w
32 31 eexd 
u = x /\ v = a -> E. y u, w = y, N[y / x] a -> v = w
33 20, 32 syl5bi 
u = x /\ v = a -> u, w e. \ x, a -> v = w
34 6, 33 sylbi 
u, v = x, a -> u, w e. \ x, a -> v = w
35 5, 34 eexh 
E. x u, v = x, a -> u, w e. \ x, a -> v = w
36 1, 35 sylbi 
u, v e. \ x, a -> u, w e. \ x, a -> v = w
37 36 ax_gen 
A. w (u, v e. \ x, a -> u, w e. \ x, a -> v = w)
38 37 ax_gen 
A. v A. w (u, v e. \ x, a -> u, w e. \ x, a -> v = w)
39 38 ax_gen 
A. u A. v A. w (u, v e. \ x, a -> u, w e. \ x, a -> v = w)
40 39 conv isfun 
isfun (\ x, a)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)