pub theorem elins (a b c: nat): $ a e. b ; c <-> a = b \/ a e. c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
2 |
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 |
conv ins |
finite {x | x = b \/ x e. c} -> (a e. b ; c <-> a e. {x | x = b \/ x e. c}) |
|
5 |
A. x (x = b \/ x e. c -> x <= max b c) <-> {x | x = b \/ x e. c} C_ {x | x <= max b c} |
||
7 |
b <= max b c |
||
8 |
x = b -> (x <= max b c <-> b <= max b c) |
||
9 |
x = b -> x <= max b c |
||
11 |
x e. c -> x < c |
||
12 |
x < c -> x <= c |
||
13 |
c <= max b c |
||
14 |
x < c -> c <= max b c |
||
15 |
x < c -> x <= max b c |
||
16 |
x e. c -> x <= max b c |
||
17 |
eor* |
x = b \/ x e. c -> x <= max b c |
|
18 |
A. x (x = b \/ x e. c -> x <= max b c) |
||
19 |
{x | x = b \/ x e. c} C_ {x | x <= max b c} |
||
21 |
finite {x | x <= max b c} |
||
22 |
finite {x | x = b \/ x e. c} |
||
23 |
a e. b ; c <-> a e. {x | x = b \/ x e. c} |
||
25 |
x = a -> (x = b <-> a = b) |
||
26 |
x = a -> (x e. c <-> a e. c) |
||
27 |
x = a -> (x = b \/ x e. c <-> a = b \/ a e. c) |
||
28 |
a e. {x | x = b \/ x e. c} <-> a = b \/ a e. c |
||
29 |
bitr* |
a e. b ; c <-> a = b \/ a e. c |