Theorem psetfn ≪ | index | src | ≫ 

theorem psetfn {a x: nat} (p: wff x) (v: nat x):
  $ finite {x | p} -> E. a A. x (p -> pset a @ x = v) $;
StepHypRefExpression
1 expset 
finite ((\ y, N[y / x] v) |` {x | p}) <-> E. a pset a == (\ y, N[y / x] v) |` {x | p}
2 finlam 
finite {x | p} -> finite ((\ y, N[y / x] v) |` {x | p})
3 1, 2 sylib 
finite {x | p} -> E. a pset a == (\ y, N[y / x] v) |` {x | p}
4 nfsv 
FS/ x pset a
5 nfsbn1 
FN/ x N[y / x] v
6 5 nflam 
FS/ x \ y, N[y / x] v
7 nfab1 
FS/ x {x | p}
8 6, 7 nfres 
FS/ x (\ y, N[y / x] v) |` {x | p}
9 4, 8 nfeqs 
F/ x pset a == (\ y, N[y / x] v) |` {x | p}
10 appeq1 
pset a == (\ y, N[y / x] v) |` {x | p} -> pset a @ x = ((\ y, N[y / x] v) |` {x | p}) @ x
11 10 anwl 
pset a == (\ y, N[y / x] v) |` {x | p} /\ p -> pset a @ x = ((\ y, N[y / x] v) |` {x | p}) @ x
12 eqtr3 
(\ x, v) @ x = (\ y, N[y / x] v) @ x -> (\ x, v) @ x = v -> (\ y, N[y / x] v) @ x = v
13 appeq1 
\ x, v == \ y, N[y / x] v -> (\ x, v) @ x = (\ y, N[y / x] v) @ x
14 cbvlams 
\ x, v == \ y, N[y / x] v
15 13, 14 ax_mp 
(\ x, v) @ x = (\ y, N[y / x] v) @ x
16 12, 15 ax_mp 
(\ x, v) @ x = v -> (\ y, N[y / x] v) @ x = v
17 applam 
(\ x, v) @ x = v
18 16, 17 ax_mp 
(\ y, N[y / x] v) @ x = v
19 abid 
x e. {x | p} <-> p
20 resapp 
x e. {x | p} -> ((\ y, N[y / x] v) |` {x | p}) @ x = (\ y, N[y / x] v) @ x
21 19, 20 sylbir 
p -> ((\ y, N[y / x] v) |` {x | p}) @ x = (\ y, N[y / x] v) @ x
22 21 anwr 
pset a == (\ y, N[y / x] v) |` {x | p} /\ p -> ((\ y, N[y / x] v) |` {x | p}) @ x = (\ y, N[y / x] v) @ x
23 18, 22 syl6eq 
pset a == (\ y, N[y / x] v) |` {x | p} /\ p -> ((\ y, N[y / x] v) |` {x | p}) @ x = v
24 11, 23 eqtrd 
pset a == (\ y, N[y / x] v) |` {x | p} /\ p -> pset a @ x = v
25 24 exp 
pset a == (\ y, N[y / x] v) |` {x | p} -> p -> pset a @ x = v
26 9, 25 ialdh 
pset a == (\ y, N[y / x] v) |` {x | p} -> A. x (p -> pset a @ x = v)
27 26 eximi 
E. a pset a == (\ y, N[y / x] v) |` {x | p} -> E. a A. x (p -> pset a @ x = v)
28 3, 27 rsyl 
finite {x | p} -> E. a A. x (p -> pset a @ x = v)

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)