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 0no ⊢ 0 s ∈ No
19 18 a1i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → 0 s ∈ No
20 bday0 ⊢ 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 bdayon ⊢ 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 elleft ⊢ d ∈ L ⁡ B ↔ d ∈ Old ⁡ bday ⁡ B ∧ d < s B
49 46 47 48 sylanbrc ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ L ⁡ B
50 fnfvima ⊢ + s Fn No ∧ L ⁡ B ⊆ No ∧ d ∈ L ⁡ B → + s ⁡ d ∈ + s L ⁡ B
51 38 39 49 50 mp3an12i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d ∈ + s L ⁡ B
52 34 37 51 sltssepcd ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ B < s + s ⁡ d
53 30 simp2d ⊢ φ → + s R ⁡ A ≪ s + s ⁡ A
54 53 adantr ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s R ⁡ A ≪ s + s ⁡ A
55 rightssno ⊢ R ⁡ A ⊆ No
56 simprr2 ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → A < s d
57 elright ⊢ d ∈ R ⁡ A ↔ d ∈ Old ⁡ bday ⁡ A ∧ A < s d
58 43 56 57 sylanbrc ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → d ∈ R ⁡ A
59 fnfvima ⊢ + s Fn No ∧ R ⁡ A ⊆ No ∧ d ∈ R ⁡ A → + s ⁡ d ∈ + s R ⁡ A
60 38 55 58 59 mp3an12i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d ∈ + s R ⁡ A
61 fvex ⊢ + s ⁡ A ∈ V
62 61 snid ⊢ + s ⁡ A ∈ + s ⁡ A
63 62 a1i ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ A ∈ + s ⁡ A
64 54 60 63 sltssepcd ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ d < s + s ⁡ A
65 15 29 32 52 64 ltstrd ⊢ φ ∧ d ∈ No ∧ bday ⁡ d ∈ bday ⁡ A ∧ A < s d ∧ d < s B → + s ⁡ B < s + s ⁡ A
66 7 65 rexlimddv ⊢ φ → + s ⁡ B < s + s ⁡ A