Theorem elins ≪ | index | src | ≫ 

pub theorem elins (a b c: nat): $ a e. b ; c <-> a = b \/ a e. c $;
StepHypRefExpression
1 bitr 
(a e. b ; c <-> a e. {x | x = b \/ x e. c}) -> (a e. {x | x = b \/ x e. c} <-> a = b \/ a e. c) -> (a e. b ; c <-> a = b \/ a e. c)
2 ellower 
finite {x | x = b \/ x e. c} -> (a e. lower {x | x = b \/ x e. c} <-> a e. {x | x = b \/ x e. c})
3 2 conv ins 
finite {x | x = b \/ x e. c} -> (a e. b ; c <-> a e. {x | x = b \/ x e. c})
4 finss 
{x | x = b \/ x e. c} C_ {x | x <= max b c} -> finite {x | x <= max b c} -> finite {x | x = b \/ x e. c}
5 ssab 
A. x (x = b \/ x e. c -> x <= max b c) <-> {x | x = b \/ x e. c} C_ {x | x <= max b c}
6 eor 
(x = b -> x <= max b c) -> (x e. c -> x <= max b c) -> x = b \/ x e. c -> x <= max b c
7 lemax1 
b <= max b c
8 leeq1 
x = b -> (x <= max b c <-> b <= max b c)
9 7, 8 mpbiri 
x = b -> x <= max b c
10 6, 9 ax_mp 
(x e. c -> x <= max b c) -> x = b \/ x e. c -> x <= max b c
11 ellt 
x e. c -> x < c
12 ltle 
x < c -> x <= c
13 lemax2 
c <= max b c
14 13 a1i 
x < c -> c <= max b c
15 12, 14 letrd 
x < c -> x <= max b c
16 11, 15 rsyl 
x e. c -> x <= max b c
17 10, 16 ax_mp 
x = b \/ x e. c -> x <= max b c
18 17 ax_gen 
A. x (x = b \/ x e. c -> x <= max b c)
19 5, 18 mpbi 
{x | x = b \/ x e. c} C_ {x | x <= max b c}
20 4, 19 ax_mp 
finite {x | x <= max b c} -> finite {x | x = b \/ x e. c}
21 lefin 
finite {x | x <= max b c}
22 20, 21 ax_mp 
finite {x | x = b \/ x e. c}
23 3, 22 ax_mp 
a e. b ; c <-> a e. {x | x = b \/ x e. c}
24 1, 23 ax_mp 
(a e. {x | x = b \/ x e. c} <-> a = b \/ a e. c) -> (a e. b ; c <-> a = b \/ a e. c)
25 eqeq1 
x = a -> (x = b <-> a = b)
26 eleq1 
x = a -> (x e. c <-> a e. c)
27 25, 26 oreqd 
x = a -> (x = b \/ x e. c <-> a = b \/ a e. c)
28 27 elabe 
a e. {x | x = b \/ x e. c} <-> a = b \/ a e. c
29 24, 28 ax_mp 
a e. b ; c <-> a = b \/ a e. c

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)