Step | Hyp | Ref | Expression |
1 |
|
bitr4 |
(all A (a ++ b) <-> A. x (x IN a ++ b -> x e. A)) -> (all A a /\ all A b <-> A. x (x IN a ++ b -> x e. A)) -> (all A (a ++ b) <-> all A a /\ all A b) |
2 |
|
allal2 |
all A (a ++ b) <-> A. x (x IN a ++ b -> x e. A) |
3 |
1, 2 |
ax_mp |
(all A a /\ all A b <-> A. x (x IN a ++ b -> x e. A)) -> (all A (a ++ b) <-> all A a /\ all A b) |
4 |
|
bitr4 |
(all A a /\ all A b <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) ->
(A. x (x IN a ++ b -> x e. A) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) ->
(all A a /\ all A b <-> A. x (x IN a ++ b -> x e. A)) |
5 |
|
aneq |
(all A a <-> A. x (x IN a -> x e. A)) -> (all A b <-> A. x (x IN b -> x e. A)) -> (all A a /\ all A b <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) |
6 |
|
allal2 |
all A a <-> A. x (x IN a -> x e. A) |
7 |
5, 6 |
ax_mp |
(all A b <-> A. x (x IN b -> x e. A)) -> (all A a /\ all A b <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) |
8 |
|
allal2 |
all A b <-> A. x (x IN b -> x e. A) |
9 |
7, 8 |
ax_mp |
all A a /\ all A b <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A) |
10 |
4, 9 |
ax_mp |
(A. x (x IN a ++ b -> x e. A) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) -> (all A a /\ all A b <-> A. x (x IN a ++ b -> x e. A)) |
11 |
|
bitr |
(A. x (x IN a ++ b -> x e. A) <-> A. x ((x IN a -> x e. A) /\ (x IN b -> x e. A))) ->
(A. x ((x IN a -> x e. A) /\ (x IN b -> x e. A)) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) ->
(A. x (x IN a ++ b -> x e. A) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) |
12 |
|
bitr |
(x IN a ++ b -> x e. A <-> x IN a \/ x IN b -> x e. A) ->
(x IN a \/ x IN b -> x e. A <-> (x IN a -> x e. A) /\ (x IN b -> x e. A)) ->
(x IN a ++ b -> x e. A <-> (x IN a -> x e. A) /\ (x IN b -> x e. A)) |
13 |
|
lmemappend |
x IN a ++ b <-> x IN a \/ x IN b |
14 |
13 |
imeq1i |
x IN a ++ b -> x e. A <-> x IN a \/ x IN b -> x e. A |
15 |
12, 14 |
ax_mp |
(x IN a \/ x IN b -> x e. A <-> (x IN a -> x e. A) /\ (x IN b -> x e. A)) -> (x IN a ++ b -> x e. A <-> (x IN a -> x e. A) /\ (x IN b -> x e. A)) |
16 |
|
imor |
x IN a \/ x IN b -> x e. A <-> (x IN a -> x e. A) /\ (x IN b -> x e. A) |
17 |
15, 16 |
ax_mp |
x IN a ++ b -> x e. A <-> (x IN a -> x e. A) /\ (x IN b -> x e. A) |
18 |
17 |
aleqi |
A. x (x IN a ++ b -> x e. A) <-> A. x ((x IN a -> x e. A) /\ (x IN b -> x e. A)) |
19 |
11, 18 |
ax_mp |
(A. x ((x IN a -> x e. A) /\ (x IN b -> x e. A)) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) ->
(A. x (x IN a ++ b -> x e. A) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A)) |
20 |
|
alan |
A. x ((x IN a -> x e. A) /\ (x IN b -> x e. A)) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A) |
21 |
19, 20 |
ax_mp |
A. x (x IN a ++ b -> x e. A) <-> A. x (x IN a -> x e. A) /\ A. x (x IN b -> x e. A) |
22 |
10, 21 |
ax_mp |
all A a /\ all A b <-> A. x (x IN a ++ b -> x e. A) |
23 |
3, 22 |
ax_mp |
all A (a ++ b) <-> all A a /\ all A b |