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

Proof

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