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 ∈ On A ⁡ x ≠ B ⁡ x ↔ ∃ x ∈ On ¬ A ⁡ x = B ⁡ x
3 2 notbii ⊢ ¬ ∃ x ∈ On A ⁡ x ≠ B ⁡ x ↔ ¬ ∃ x ∈ On ¬ A ⁡ x = B ⁡ x
4 dfral2 ⊢ ∀ x ∈ On A ⁡ x = B ⁡ x ↔ ¬ ∃ x ∈ On ¬ A ⁡ x = B ⁡ x
5 3 4 bitr4i ⊢ ¬ ∃ x ∈ On A ⁡ x ≠ B ⁡ x ↔ ∀ x ∈ On A ⁡ 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 ∈ On A ⁡ x = B ⁡ x
16 15 3expia ⊢ A ∈ No ∧ B ∈ No → dom ⁡ A ∈ dom ⁡ B → ¬ ∀ x ∈ On A ⁡ x = B ⁡ x
17 noseponlem ⊢ B ∈ No ∧ A ∈ No ∧ dom ⁡ B ∈ dom ⁡ A → ¬ ∀ x ∈ On B ⁡ x = A ⁡ x
18 eqcom ⊢ A ⁡ x = B ⁡ x ↔ B ⁡ x = A ⁡ x
19 18 ralbii ⊢ ∀ x ∈ On A ⁡ x = B ⁡ x ↔ ∀ x ∈ On B ⁡ x = A ⁡ x
20 17 19 sylnibr ⊢ B ∈ No ∧ A ∈ No ∧ dom ⁡ B ∈ dom ⁡ A → ¬ ∀ x ∈ On A ⁡ x = B ⁡ x
21 20 3expia ⊢ B ∈ No ∧ A ∈ No → dom ⁡ B ∈ dom ⁡ A → ¬ ∀ x ∈ On A ⁡ x = B ⁡ x
22 21 ancoms ⊢ A ∈ No ∧ B ∈ No → dom ⁡ B ∈ dom ⁡ A → ¬ ∀ x ∈ On A ⁡ x = B ⁡ x
23 16 22 jaod ⊢ A ∈ No ∧ B ∈ No → dom ⁡ A ∈ dom ⁡ B ∨ dom ⁡ B ∈ dom ⁡ A → ¬ ∀ x ∈ On A ⁡ x = B ⁡ x
24 14 23 syld ⊢ A ∈ No ∧ B ∈ No → ¬ dom ⁡ A = dom ⁡ B → ¬ ∀ x ∈ On A ⁡ x = B ⁡ x
25 24 con4d ⊢ A ∈ No ∧ B ∈ No → ∀ x ∈ On A ⁡ x = B ⁡ x → dom ⁡ A = dom ⁡ B
26 25 3impia ⊢ A ∈ No ∧ B ∈ No ∧ ∀ x ∈ On A ⁡ x = B ⁡ x → dom ⁡ A = dom ⁡ B
27 ordsson ⊢ Ord ⁡ dom ⁡ A → dom ⁡ A ⊆ On
28 ssralv ⊢ dom ⁡ A ⊆ On → ∀ x ∈ On A ⁡ x = B ⁡ x → ∀ x ∈ dom ⁡ A A ⁡ x = B ⁡ x
29 6 27 28 3syl ⊢ A ∈ No → ∀ x ∈ On A ⁡ x = B ⁡ x → ∀ x ∈ dom ⁡ A A ⁡ x = B ⁡ x
30 29 adantr ⊢ A ∈ No ∧ B ∈ No → ∀ x ∈ On A ⁡ x = B ⁡ x → ∀ x ∈ dom ⁡ A A ⁡ x = B ⁡ x
31 30 3impia ⊢ A ∈ No ∧ B ∈ No ∧ ∀ x ∈ On A ⁡ x = B ⁡ x → ∀ x ∈ dom ⁡ A A ⁡ x = B ⁡ x
32 nofun ⊢ A ∈ No → Fun ⁡ A
33 32 3ad2ant1 ⊢ A ∈ No ∧ B ∈ No ∧ ∀ x ∈ On A ⁡ x = B ⁡ x → Fun ⁡ A
34 nofun ⊢ B ∈ No → Fun ⁡ B
35 34 3ad2ant2 ⊢ A ∈ No ∧ B ∈ No ∧ ∀ x ∈ On A ⁡ x = B ⁡ x → Fun ⁡ B
36 eqfunfv ⊢ Fun ⁡ A ∧ Fun ⁡ B → A = B ↔ dom ⁡ A = dom ⁡ B ∧ ∀ x ∈ dom ⁡ A A ⁡ x = B ⁡ x
37 33 35 36 syl2anc ⊢ A ∈ No ∧ B ∈ No ∧ ∀ x ∈ On A ⁡ x = B ⁡ x → A = B ↔ dom ⁡ A = dom ⁡ B ∧ ∀ x ∈ dom ⁡ A A ⁡ x = B ⁡ x
38 26 31 37 mpbir2and ⊢ A ∈ No ∧ B ∈ No ∧ ∀ x ∈ On A ⁡ x = B ⁡ x → A = B
39 38 3expia ⊢ A ∈ No ∧ B ∈ No → ∀ x ∈ On A ⁡ x = B ⁡ x → A = B
40 5 39 syl5bi ⊢ A ∈ No ∧ B ∈ No → ¬ ∃ x ∈ On A ⁡ x ≠ B ⁡ x → A = B
41 40 necon1ad ⊢ A ∈ No ∧ B ∈ No → A ≠ B → ∃ x ∈ On A ⁡ x ≠ B ⁡ x
42 41 3impia ⊢ A ∈ No ∧ B ∈ No ∧ A ≠ B → ∃ x ∈ On A ⁡ x ≠ B ⁡ x
43 onintrab2 ⊢ ∃ x ∈ On A ⁡ 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