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