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<sB→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<sB→A∈No
2 simplr ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→B∈No
3 sltso ⊢<sOrNo
4 sonr ⊢<sOrNo∧A∈No→¬A<sA
5 3 4 mpan ⊢A∈No→¬A<sA
6 breq2 ⊢A=B→A<sA↔A<sB
7 6 notbid ⊢A=B→¬A<sA↔¬A<sB
8 5 7 syl5ibcom ⊢A∈No→A=B→¬A<sB
9 8 necon2ad ⊢A∈No→A<sB→A≠B
10 9 imp ⊢A∈No∧A<sB→A≠B
11 10 ad2ant2rl ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A≠B
12 1 2 11 3jca ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→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<sB∧C∈⋂a∈On|A⁡a≠B⁡a→A⁡C=B⁡C
15 14 ex ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→C∈⋂a∈On|A⁡a≠B⁡a→A⁡C=B⁡C