Metamath Proof Explorer

Theorem nodenselem4

Description: Lemma for nodense . Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion nodenselem4 ⊢A∈No∧B∈No∧A<sB→⋂a∈On|A⁡a≠B⁡a∈On

Proof

Step Hyp Ref Expression
1 simpll ⊢A∈No∧B∈No∧A<sB→A∈No
2 simplr ⊢A∈No∧B∈No∧A<sB→B∈No
3 sltso ⊢<sOrNo
4 sonr ⊢<sOrNo∧A∈No→¬A<sA
5 3 4 mpan ⊢A∈No→¬A<sA
6 5 adantr ⊢A∈No∧B∈No→¬A<sA
7 breq2 ⊢A=B→A<sA↔A<sB
8 7 notbid ⊢A=B→¬A<sA↔¬A<sB
9 6 8 syl5ibcom ⊢A∈No∧B∈No→A=B→¬A<sB
10 9 necon2ad ⊢A∈No∧B∈No→A<sB→A≠B
11 10 imp ⊢A∈No∧B∈No∧A<sB→A≠B
12 nosepon ⊢A∈No∧B∈No∧A≠B→⋂a∈On|A⁡a≠B⁡a∈On
13 1 2 11 12 syl3anc ⊢A∈No∧B∈No∧A<sB→⋂a∈On|A⁡a≠B⁡a∈On