Metamath Proof Explorer

Theorem nosepon

Description: Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020)

Ref Expression
Assertion nosepon ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ On )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
2 1 rexbii ⊢ ( ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
3 2 notbii ⊢ ( ¬ ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ On ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
4 dfral2 ⊢ ( ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ On ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
5 3 4 bitr4i ⊢ ( ¬ ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
6 nodmord ⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )
7 nodmord ⊢ ( 𝐵 ∈ No → Ord dom 𝐵 )
8 ordtri3or ⊢ ( ( Ord dom 𝐴 ∧ Ord dom 𝐵 ) → ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) )
9 6 7 8 syl2an ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) )
10 3orass ⊢ ( ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ↔ ( dom 𝐴 ∈ dom 𝐵 ∨ ( dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ) )
11 or12 ⊢ ( ( dom 𝐴 ∈ dom 𝐵 ∨ ( dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ) ↔ ( dom 𝐴 = dom 𝐵 ∨ ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ) )
12 10 11 bitri ⊢ ( ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ↔ ( dom 𝐴 = dom 𝐵 ∨ ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ) )
13 9 12 sylib ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( dom 𝐴 = dom 𝐵 ∨ ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ) )
14 13 ord ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ¬ dom 𝐴 = dom 𝐵 → ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) ) )
15 noseponlem ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
16 15 3expia ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( dom 𝐴 ∈ dom 𝐵 → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
17 noseponlem ⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ∧ dom 𝐵 ∈ dom 𝐴 ) → ¬ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
18 eqcom ⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐵 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
19 18 ralbii ⊢ ( ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
20 17 19 sylnibr ⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ∧ dom 𝐵 ∈ dom 𝐴 ) → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
21 20 3expia ⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( dom 𝐵 ∈ dom 𝐴 → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
22 21 ancoms ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( dom 𝐵 ∈ dom 𝐴 → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
23 16 22 jaod ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴 ) → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
24 14 23 syld ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ¬ dom 𝐴 = dom 𝐵 → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
25 24 con4d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → dom 𝐴 = dom 𝐵 ) )
26 25 3impia ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → dom 𝐴 = dom 𝐵 )
27 ordsson ⊢ ( Ord dom 𝐴 → dom 𝐴 ⊆ On )
28 ssralv ⊢ ( dom 𝐴 ⊆ On → ( ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ∀ 𝑥 ∈ dom 𝐴 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
29 6 27 28 3syl ⊢ ( 𝐴 ∈ No → ( ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ∀ 𝑥 ∈ dom 𝐴 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
30 29 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → ∀ 𝑥 ∈ dom 𝐴 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
31 30 3impia ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ dom 𝐴 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
32 nofun ⊢ ( 𝐴 ∈ No → Fun 𝐴 )
33 32 3ad2ant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → Fun 𝐴 )
34 nofun ⊢ ( 𝐵 ∈ No → Fun 𝐵 )
35 34 3ad2ant2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → Fun 𝐵 )
36 eqfunfv ⊢ ( ( Fun 𝐴 ∧ Fun 𝐵 ) → ( 𝐴 = 𝐵 ↔ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐴 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) ) )
37 33 35 36 syl2anc ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → ( 𝐴 = 𝐵 ↔ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐴 ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) ) )
38 26 31 37 mpbir2and ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) → 𝐴 = 𝐵 )
39 38 3expia ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) → 𝐴 = 𝐵 ) )
40 5 39 biimtrid ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ¬ ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) → 𝐴 = 𝐵 ) )
41 40 necon1ad ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≠ 𝐵 → ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ) )
42 41 3impia ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) )
43 onintrab2 ⊢ ( ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ On )
44 42 43 sylib ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ On )