Metamath Proof Explorer


Theorem ackbij1lem1

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion ackbij1lem1 ¬ A B B suc A = B A

Proof

Step Hyp Ref Expression
1 df-suc suc A = A A
2 1 ineq2i B suc A = B A A
3 indi B A A = B A B A
4 2 3 eqtri B suc A = B A B A
5 disjsn B A = ¬ A B
6 5 biimpri ¬ A B B A =
7 6 uneq2d ¬ A B B A B A = B A
8 un0 B A = B A
9 7 8 syl6eq ¬ A B B A B A = B A
10 4 9 syl5eq ¬ A B B suc A = B A