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 < s B → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ On

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ No ∧ B ∈ No ∧ A < s B → A ∈ No
2 simplr ⊢ A ∈ No ∧ B ∈ No ∧ 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 5 adantr ⊢ A ∈ No ∧ B ∈ No → ¬ A < s A
7 breq2 ⊢ A = B → A < s A ↔ A < s B
8 7 notbid ⊢ A = B → ¬ A < s A ↔ ¬ A < s B
9 6 8 syl5ibcom ⊢ A ∈ No ∧ B ∈ No → A = B → ¬ A < s B
10 9 necon2ad ⊢ A ∈ No ∧ B ∈ No → A < s B → A ≠ B
11 10 imp ⊢ A ∈ No ∧ B ∈ No ∧ A < s B → 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 < s B → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ On