Metamath Proof Explorer


Theorem nodenselem7

Description: Lemma for nodense . A and B are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011)

Ref Expression
Assertion nodenselem7 A No B No bday A = bday B A < s B C a On | A a B a A C = B C

Proof

Step Hyp Ref Expression
1 simpll A No B No bday A = bday B A < s B A No
2 simplr A No B No bday A = bday B A < s B B No
3 sltso < s Or No
4 sonr < s Or No A No ¬ A < s A
5 3 4 mpan A No ¬ A < s A
6 breq2 A = B A < s A A < s B
7 6 notbid A = B ¬ A < s A ¬ A < s B
8 5 7 syl5ibcom A No A = B ¬ A < s B
9 8 necon2ad A No A < s B A B
10 9 imp A No A < s B A B
11 10 ad2ant2rl A No B No bday A = bday B A < s B A B
12 1 2 11 3jca A No B No bday A = bday B A < s B A No B No A B
13 nosepeq A No B No A B C a On | A a B a A C = B C
14 12 13 sylan A No B No bday A = bday B A < s B C a On | A a B a A C = B C
15 14 ex A No B No bday A = bday B A < s B C a On | A a B a A C = B C