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 ⊢A∈No∧B∈No∧A≠B→⋂x∈On|A⁡x≠B⁡x∈On

Proof

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