Theorem psetsep ≪ | index | src | ≫ 

theorem psetsep {b: nat} (n: nat) {x: nat} (p: wff x):
  $ E. b pset b == {x | x < n /\ p} $;
StepHypRefExpression
1 id 
_1 = n -> _1 = n
2 1 lteq2d 
_1 = n -> (x < _1 <-> x < n)
3 2 aneq1d 
_1 = n -> (x < _1 /\ p <-> x < n /\ p)
4 3 abeqd 
_1 = n -> {x | x < _1 /\ p} == {x | x < n /\ p}
5 4 eqseq2d 
_1 = n -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < n /\ p})
6 5 aneq2d 
_1 = n -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < n /\ p})
7 6 exeqd 
_1 = n -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < n /\ p}))
8 id 
_1 = 0 -> _1 = 0
9 8 lteq2d 
_1 = 0 -> (x < _1 <-> x < 0)
10 9 aneq1d 
_1 = 0 -> (x < _1 /\ p <-> x < 0 /\ p)
11 10 abeqd 
_1 = 0 -> {x | x < _1 /\ p} == {x | x < 0 /\ p}
12 11 eqseq2d 
_1 = 0 -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < 0 /\ p})
13 12 aneq2d 
_1 = 0 -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < 0 /\ p})
14 13 exeqd 
_1 = 0 -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p}))
15 id 
_1 = v -> _1 = v
16 15 lteq2d 
_1 = v -> (x < _1 <-> x < v)
17 16 aneq1d 
_1 = v -> (x < _1 /\ p <-> x < v /\ p)
18 17 abeqd 
_1 = v -> {x | x < _1 /\ p} == {x | x < v /\ p}
19 18 eqseq2d 
_1 = v -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < v /\ p})
20 19 aneq2d 
_1 = v -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < v /\ p})
21 20 exeqd 
_1 = v -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}))
22 id 
_1 = suc v -> _1 = suc v
23 22 lteq2d 
_1 = suc v -> (x < _1 <-> x < suc v)
24 23 aneq1d 
_1 = suc v -> (x < _1 /\ p <-> x < suc v /\ p)
25 24 abeqd 
_1 = suc v -> {x | x < _1 /\ p} == {x | x < suc v /\ p}
26 25 eqseq2d 
_1 = suc v -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < suc v /\ p})
27 26 aneq2d 
_1 = suc v -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < suc v /\ p})
28 27 exeqd 
_1 = suc v -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p}))
29 lteq2 
a = 1 -> (0 < a <-> 0 < 1)
30 preq2 
a = 1 -> m, a = m, 1
31 30 pseteqd 
a = 1 -> pset (m, a) == pset (m, 1)
32 31 eqseq1d 
a = 1 -> (pset (m, a) == {x | x < 0 /\ p} <-> pset (m, 1) == {x | x < 0 /\ p})
33 29, 32 aneqd 
a = 1 -> (0 < a /\ pset (m, a) == {x | x < 0 /\ p} <-> 0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p})
34 33 iexe 
0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p} -> E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p})
35 ian 
0 < 1 -> pset (m, 1) == {x | x < 0 /\ p} -> 0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p}
36 d0lt1 
0 < 1
37 35, 36 ax_mp 
pset (m, 1) == {x | x < 0 /\ p} -> 0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p}
38 binth 
~x e. pset (m, 1) -> ~(x < 0 /\ p) -> (x e. pset (m, 1) <-> x < 0 /\ p)
39 elpset1 
~x e. pset (m, 1)
40 38, 39 ax_mp 
~(x < 0 /\ p) -> (x e. pset (m, 1) <-> x < 0 /\ p)
41 anl 
x < 0 /\ p -> x < 0
42 lt02 
~x < 0
43 41, 42 mt 
~(x < 0 /\ p)
44 40, 43 ax_mp 
x e. pset (m, 1) <-> x < 0 /\ p
45 44 eqab2i 
pset (m, 1) == {x | x < 0 /\ p}
46 37, 45 ax_mp 
0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p}
47 34, 46 ax_mp 
E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p})
48 47 a1i 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p})
49 lteq2 
a = b -> (0 < a <-> 0 < b)
50 preq2 
a = b -> m, a = m, b
51 50 pseteqd 
a = b -> pset (m, a) == pset (m, b)
52 51 eqseq1d 
a = b -> (pset (m, a) == {x | x < suc v /\ p} <-> pset (m, b) == {x | x < suc v /\ p})
53 49, 52 aneqd 
a = b -> (0 < a /\ pset (m, a) == {x | x < suc v /\ p} <-> 0 < b /\ pset (m, b) == {x | x < suc v /\ p})
54 53 cbvex 
E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p}) <-> E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})
55 lteq2 
b = a * suc (m * suc v) -> (0 < b <-> 0 < a * suc (m * suc v))
56 preq2 
b = a * suc (m * suc v) -> m, b = m, a * suc (m * suc v)
57 56 pseteqd 
b = a * suc (m * suc v) -> pset (m, b) == pset (m, a * suc (m * suc v))
58 57 eqseq1d 
b = a * suc (m * suc v) -> (pset (m, b) == {x | x < suc v /\ p} <-> pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p})
59 55, 58 aneqd 
b = a * suc (m * suc v) -> (0 < b /\ pset (m, b) == {x | x < suc v /\ p} <-> 0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p})
60 59 iexe 
0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p} -> E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})
61 mulpos 
0 < a * suc (m * suc v) <-> 0 < a /\ 0 < suc (m * suc v)
62 anrl 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < a
63 lt01S 
0 < suc (m * suc v)
64 63 a1i 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < suc (m * suc v)
65 62, 64 iand 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < a /\ 0 < suc (m * suc v)
66 61, 65 sylibr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < a * suc (m * suc v)
67 bitr 
(y e. {x | x < suc v /\ p} <-> [y / x] (x < suc v /\ p)) ->
  ([y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p) ->
  (y e. {x | x < suc v /\ p} <-> y < suc v /\ [y / x] p)
68 elab 
y e. {x | x < suc v /\ p} <-> [y / x] (x < suc v /\ p)
69 67, 68 ax_mp 
([y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p) -> (y e. {x | x < suc v /\ p} <-> y < suc v /\ [y / x] p)
70 nfv 
F/ x y < suc v
71 nfsb1 
F/ x [y / x] p
72 70, 71 nfan 
F/ x y < suc v /\ [y / x] p
73 lteq1 
x = y -> (x < suc v <-> y < suc v)
74 sbq 
x = y -> (p <-> [y / x] p)
75 73, 74 aneqd 
x = y -> (x < suc v /\ p <-> y < suc v /\ [y / x] p)
76 72, 75 sbeh 
[y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p
77 69, 76 ax_mp 
y e. {x | x < suc v /\ p} <-> y < suc v /\ [y / x] p
78 an3l 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < m /\ A. x (0 < x /\ x <= n -> x || m)
79 78 anld 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < m
80 lteq2 
x = z -> (0 < x <-> 0 < z)
81 leeq1 
x = z -> (x <= v <-> z <= v)
82 80, 81 aneqd 
x = z -> (0 < x /\ x <= v <-> 0 < z /\ z <= v)
83 dvdeq1 
x = z -> (x || m <-> z || m)
84 82, 83 imeqd 
x = z -> (0 < x /\ x <= v -> x || m <-> 0 < z /\ z <= v -> z || m)
85 84 cbval 
A. x (0 < x /\ x <= v -> x || m) <-> A. z (0 < z /\ z <= v -> z || m)
86 78 anrd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> A. x (0 < x /\ x <= n -> x || m)
87 letr 
v <= suc v -> suc v <= n -> v <= n
88 lesucid 
v <= suc v
89 87, 88 ax_mp 
suc v <= n -> v <= n
90 anllr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> v < n
91 90 conv lt 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> suc v <= n
92 89, 91 syl 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> v <= n
93 letr 
x <= v -> v <= n -> x <= n
94 93 com12 
v <= n -> x <= v -> x <= n
95 94 anim2d 
v <= n -> 0 < x /\ x <= v -> 0 < x /\ x <= n
96 95 imim1d 
v <= n -> (0 < x /\ x <= n -> x || m) -> 0 < x /\ x <= v -> x || m
97 96 alimd 
v <= n -> A. x (0 < x /\ x <= n -> x || m) -> A. x (0 < x /\ x <= v -> x || m)
98 92, 97 rsyl 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  A. x (0 < x /\ x <= n -> x || m) ->
  A. x (0 < x /\ x <= v -> x || m)
99 86, 98 mpd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> A. x (0 < x /\ x <= v -> x || m)
100 85, 99 sylib 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> A. z (0 < z /\ z <= v -> z || m)
101 79, 62, 100 psetS 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a * suc (m * suc v)) <-> y e. pset (m, a) \/ y = v)
102 bitr 
(y e. {x | x < v /\ p} <-> [y / x] (x < v /\ p)) -> ([y / x] (x < v /\ p) <-> y < v /\ [y / x] p) -> (y e. {x | x < v /\ p} <-> y < v /\ [y / x] p)
103 elab 
y e. {x | x < v /\ p} <-> [y / x] (x < v /\ p)
104 102, 103 ax_mp 
([y / x] (x < v /\ p) <-> y < v /\ [y / x] p) -> (y e. {x | x < v /\ p} <-> y < v /\ [y / x] p)
105 nfv 
F/ x y < v
106 105, 71 nfan 
F/ x y < v /\ [y / x] p
107 lteq1 
x = y -> (x < v <-> y < v)
108 107, 74 aneqd 
x = y -> (x < v /\ p <-> y < v /\ [y / x] p)
109 106, 108 sbeh 
[y / x] (x < v /\ p) <-> y < v /\ [y / x] p
110 104, 109 ax_mp 
y e. {x | x < v /\ p} <-> y < v /\ [y / x] p
111 anrr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> pset (m, a) == {x | x < v /\ p}
112 111 eleq2d 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> (y e. pset (m, a) <-> y e. {x | x < v /\ p})
113 110, 112 syl6bb 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> (y e. pset (m, a) <-> y < v /\ [y / x] p)
114 113 oreq1d 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a) \/ y = v <-> y < v /\ [y / x] p \/ y = v)
115 bitr 
(y < suc v /\ [y / x] p <-> (y < v \/ y = v) /\ [y / x] p) ->
  ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) ->
  (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
116 bitr3 
(y <= v <-> y < suc v) -> (y <= v <-> y < v \/ y = v) -> (y < suc v <-> y < v \/ y = v)
117 leltsuc 
y <= v <-> y < suc v
118 116, 117 ax_mp 
(y <= v <-> y < v \/ y = v) -> (y < suc v <-> y < v \/ y = v)
119 leloe 
y <= v <-> y < v \/ y = v
120 118, 119 ax_mp 
y < suc v <-> y < v \/ y = v
121 120 aneq1i 
y < suc v /\ [y / x] p <-> (y < v \/ y = v) /\ [y / x] p
122 115, 121 ax_mp 
((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
123 bitr 
((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [y / x] p) ->
  (y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) ->
  ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
124 andir 
(y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [y / x] p
125 123, 124 ax_mp 
(y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) ->
  ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
126 aneq2a 
(y = v -> ([y / x] p <-> [v / x] p)) -> (y = v /\ [y / x] p <-> y = v /\ [v / x] p)
127 sbeq1 
y = v -> ([y / x] p <-> [v / x] p)
128 126, 127 ax_mp 
y = v /\ [y / x] p <-> y = v /\ [v / x] p
129 128 oreq2i 
y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p
130 125, 129 ax_mp 
(y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p
131 122, 130 ax_mp 
y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p
132 bian2 
[v / x] p -> (y = v /\ [v / x] p <-> y = v)
133 anlr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> [v / x] p
134 132, 133 syl 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> (y = v /\ [v / x] p <-> y = v)
135 134 oreq2d 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p \/ y = v)
136 131, 135 syl5bb 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v)
137 114, 136 bitr4d 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a) \/ y = v <-> y < suc v /\ [y / x] p)
138 101, 137 bitrd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a * suc (m * suc v)) <-> y < suc v /\ [y / x] p)
139 77, 138 syl6bbr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a * suc (m * suc v)) <-> y e. {x | x < suc v /\ p})
140 139 eqrd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p}
141 66, 140 iand 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p}
142 60, 141 syl 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})
143 142 eexda 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p ->
  E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})
144 54, 143 syl6ibr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p ->
  E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})
145 bior2 
~(y = v /\ [v / x] p) -> (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p)
146 con3 
(y = v /\ [v / x] p -> [v / x] p) -> ~[v / x] p -> ~(y = v /\ [v / x] p)
147 anr 
y = v /\ [v / x] p -> [v / x] p
148 146, 147 ax_mp 
~[v / x] p -> ~(y = v /\ [v / x] p)
149 148 anwr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> ~(y = v /\ [v / x] p)
150 145, 149 syl 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p)
151 131, 150 syl5bb 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p)
152 110, 151 syl6bbr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y < suc v /\ [y / x] p <-> y e. {x | x < v /\ p})
153 77, 152 syl5bb 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y e. {x | x < suc v /\ p} <-> y e. {x | x < v /\ p})
154 153 eqrd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> {x | x < suc v /\ p} == {x | x < v /\ p}
155 154 eqseq2d 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (pset (m, a) == {x | x < suc v /\ p} <-> pset (m, a) == {x | x < v /\ p})
156 155 aneq2d 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (0 < a /\ pset (m, a) == {x | x < suc v /\ p} <-> 0 < a /\ pset (m, a) == {x | x < v /\ p})
157 156 exeqd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p ->
  (E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}))
158 157 bi2d 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p ->
  E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})
159 144, 158 casesda 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n -> E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})
160 159 imp 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})
161 7, 14, 21, 28, 48, 160 indlt 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. a (0 < a /\ pset (m, a) == {x | x < n /\ p})
162 pseteq 
b = m, a -> pset b == pset (m, a)
163 162 anwr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) /\ b = m, a -> pset b == pset (m, a)
164 anrr 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) -> pset (m, a) == {x | x < n /\ p}
165 164 anwl 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) /\ b = m, a -> pset (m, a) == {x | x < n /\ p}
166 163, 165 eqstrd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) /\ b = m, a -> pset b == {x | x < n /\ p}
167 166 iexde 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) -> E. b pset b == {x | x < n /\ p}
168 167 eexda 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. a (0 < a /\ pset (m, a) == {x | x < n /\ p}) -> E. b pset b == {x | x < n /\ p}
169 161, 168 mpd 
0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. b pset b == {x | x < n /\ p}
170 169 eex 
E. m (0 < m /\ A. x (0 < x /\ x <= n -> x || m)) -> E. b pset b == {x | x < n /\ p}
171 lcmex 
E. m (0 < m /\ A. x (0 < x /\ x <= n -> x || m))
172 170, 171 ax_mp 
E. b pset b == {x | x < n /\ p}

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)