Metamath Proof Explorer

Theorem negsproplem6

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is the same age as B . (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Hypotheses negsproplem.1 ⊢ φ → ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ A ∪ bday ⁡ B → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
negsproplem4.1 ⊢ φ → A ∈ No
negsproplem4.2 ⊢ φ → B ∈ No
negsproplem4.3 ⊢ φ → A < s B
negsproplem6.4 ⊢ φ → bday ⁡ A = bday ⁡ B
Assertion negsproplem6 ⊢ φ → + s ⁡ B < s + s ⁡ A

Proof

Step Hyp Ref Expression
1 negsproplem.1 ⊢ φ → ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ A ∪ bday ⁡ B → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
2 negsproplem4.1 ⊢ φ → A ∈ No
3 negsproplem4.2 ⊢ φ → B ∈ No
4 negsproplem4.3 ⊢ φ → A < s B
5 negsproplem6.4 ⊢ φ → bday ⁡ A = bday ⁡ B
6 nodense ⊢ A ∈ No ∧ B ∈ No ∧ bday ⁡ A = bday ⁡ B ∧ A < s B → ∃ d ∈ No bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B
7 2 3 5 4 6 syl22anc ⊢ φ → ∃ d ∈ No bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B
8 uncom ⊢ bday ⁡ A ∪ bday ⁡ B = bday ⁡ B ∪ bday ⁡ A
9 8 eleq2i ⊢ bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ A ∪ bday ⁡ B ↔ bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ B ∪ bday ⁡ A
10 9 imbi1i ⊢ bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ A ∪ bday ⁡ B → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ B ∪ bday ⁡ A → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
11 10 2ralbii ⊢ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ A ∪ bday ⁡ B → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ B ∪ bday ⁡ A → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
12 1 11 sylib ⊢ φ → ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ B ∪ bday ⁡ A → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
13 12 3 negsproplem3 ⊢ φ → + s ⁡ B ∈ No ∧ + s R ⁡ B ≪ s + s ⁡ B ∧ + s ⁡ B ≪ s + s L ⁡ B
14 13 simp1d ⊢ φ → + s ⁡ B ∈ No
15 14 adantr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ B ∈ No
16 1 adantr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ A ∪ bday ⁡ B → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
17 simprl ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ No
18 0sno ⊢ 0 s ∈ No
19 18 a1i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → 0 s ∈ No
20 bday0s ⊢ bday ⁡ 0 s = ∅
21 20 uneq2i ⊢ bday ⁡ d ∪ bday ⁡ 0 s = bday ⁡ d ∪ ∅
22 un0 ⊢ bday ⁡ d ∪ ∅ = bday ⁡ d
23 21 22 eqtri ⊢ bday ⁡ d ∪ bday ⁡ 0 s = bday ⁡ d
24 simprr1 ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → bday ⁡ d ∈ bday ⁡ A
25 elun1 ⊢ bday ⁡ d ∈ bday ⁡ A → bday ⁡ d ∈ bday ⁡ A ∪ bday ⁡ B
26 24 25 syl ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → bday ⁡ d ∈ bday ⁡ A ∪ bday ⁡ B
27 23 26 eqeltrid ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → bday ⁡ d ∪ bday ⁡ 0 s ∈ bday ⁡ A ∪ bday ⁡ B
28 16 17 19 27 negsproplem1 ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d ∈ No ∧ d < s 0 s → + s ⁡ 0 s < s + s ⁡ d
29 28 simpld ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d ∈ No
30 1 2 negsproplem3 ⊢ φ → + s ⁡ A ∈ No ∧ + s R ⁡ A ≪ s + s ⁡ A ∧ + s ⁡ A ≪ s + s L ⁡ A
31 30 simp1d ⊢ φ → + s ⁡ A ∈ No
32 31 adantr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ A ∈ No
33 13 simp3d ⊢ φ → + s ⁡ B ≪ s + s L ⁡ B
34 33 adantr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ B ≪ s + s L ⁡ B
35 fvex ⊢ + s ⁡ B ∈ V
36 35 snid ⊢ + s ⁡ B ∈ + s ⁡ B
37 36 a1i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ B ∈ + s ⁡ B
38 negsfn ⊢ + s Fn No
39 leftssno ⊢ L ⁡ B ⊆ No
40 bdayelon ⊢ bday ⁡ A ∈ On
41 oldbday ⊢ bday ⁡ A ∈ On ∧ d ∈ No → d ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ d ∈ bday ⁡ A
42 40 17 41 sylancr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ d ∈ bday ⁡ A
43 24 42 mpbird ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ Old ⁡ bday ⁡ A
44 5 fveq2d ⊢ φ → Old ⁡ bday ⁡ A = Old ⁡ bday ⁡ B
45 44 adantr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → Old ⁡ bday ⁡ A = Old ⁡ bday ⁡ B
46 43 45 eleqtrd ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ Old ⁡ bday ⁡ B
47 simprr3 ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d < s B
48 leftval ⊢ L ⁡ B = d ∈ Old ⁡ bday ⁡ B | d < s B
49 48 reqabi ⊢ d ∈ L ⁡ B ↔ d ∈ Old ⁡ bday ⁡ B ∧ d < s B
50 46 47 49 sylanbrc ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ L ⁡ B
51 fnfvima ⊢ + s Fn No ∧ L ⁡ B ⊆ No ∧ d ∈ L ⁡ B → + s ⁡ d ∈ + s L ⁡ B
52 38 39 50 51 mp3an12i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d ∈ + s L ⁡ B
53 34 37 52 ssltsepcd ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ B < s + s ⁡ d
54 30 simp2d ⊢ φ → + s R ⁡ A ≪ s + s ⁡ A
55 54 adantr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s R ⁡ A ≪ s + s ⁡ A
56 rightssno ⊢ R ⁡ A ⊆ No
57 simprr2 ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → A < s d
58 rightval ⊢ R ⁡ A = d ∈ Old ⁡ bday ⁡ A | A < s d
59 58 reqabi ⊢ d ∈ R ⁡ A ↔ d ∈ Old ⁡ bday ⁡ A ∧ A < s d
60 43 57 59 sylanbrc ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ R ⁡ A
61 fnfvima ⊢ + s Fn No ∧ R ⁡ A ⊆ No ∧ d ∈ R ⁡ A → + s ⁡ d ∈ + s R ⁡ A
62 38 56 60 61 mp3an12i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d ∈ + s R ⁡ A
63 fvex ⊢ + s ⁡ A ∈ V
64 63 snid ⊢ + s ⁡ A ∈ + s ⁡ A
65 64 a1i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ A ∈ + s ⁡ A
66 55 62 65 ssltsepcd ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d < s + s ⁡ A
67 15 29 32 53 66 slttrd ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ B < s + s ⁡ A
68 7 67 rexlimddv ⊢ φ → + s ⁡ B < s + s ⁡ A