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	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐶 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝐶 ) = ( 𝐵 ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 ∈ No )
2		simplr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐵 ∈ No )
3		sltso	⊢ <s Or No
4		sonr	⊢ ( ( <s Or No ∧ 𝐴 ∈ No ) → ¬ 𝐴 <s 𝐴 )
5	3 4	mpan	⊢ ( 𝐴 ∈ No → ¬ 𝐴 <s 𝐴 )
6		breq2	⊢ ( 𝐴 = 𝐵 → ( 𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵 ) )
7	6	notbid	⊢ ( 𝐴 = 𝐵 → ( ¬ 𝐴 <s 𝐴 ↔ ¬ 𝐴 <s 𝐵 ) )
8	5 7	syl5ibcom	⊢ ( 𝐴 ∈ No → ( 𝐴 = 𝐵 → ¬ 𝐴 <s 𝐵 ) )
9	8	necon2ad	⊢ ( 𝐴 ∈ No → ( 𝐴 <s 𝐵 → 𝐴 ≠ 𝐵 ) )
10	9	imp	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 <s 𝐵 ) → 𝐴 ≠ 𝐵 )
11	10	ad2ant2rl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 ≠ 𝐵 )
12	1 2 11	3jca	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) )
13		nosepeq	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝐴 ‘ 𝐶 ) = ( 𝐵 ‘ 𝐶 ) )
14	12 13	sylan	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) ∧ 𝐶 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝐴 ‘ 𝐶 ) = ( 𝐵 ‘ 𝐶 ) )
15	14	ex	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐶 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝐶 ) = ( 𝐵 ‘ 𝐶 ) ) )