Metamath Proof Explorer

Theorem negsprop

Description: Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsprop ⊢ A ∈ No ∧ B ∈ No → + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A

Proof

Step Hyp Ref Expression
1 bdayelon ⊢ bday ⁡ A ∈ On
2 bdayelon ⊢ bday ⁡ B ∈ On
3 1 2 onun2i ⊢ bday ⁡ A ∪ bday ⁡ B ∈ On
4 risset ⊢ bday ⁡ A ∪ bday ⁡ B ∈ On ↔ ∃ a ∈ On a = bday ⁡ A ∪ bday ⁡ B
5 3 4 mpbi ⊢ ∃ a ∈ On a = bday ⁡ A ∪ bday ⁡ B
6 eqeq1 ⊢ a = b → a = bday ⁡ p ∪ bday ⁡ q ↔ b = bday ⁡ p ∪ bday ⁡ q
7 6 imbi1d ⊢ a = b → a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ b = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
8 7 2ralbidv ⊢ a = b → ∀ p ∈ No ∀ q ∈ No a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ ∀ p ∈ No ∀ q ∈ No b = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
9 fveq2 ⊢ p = x → bday ⁡ p = bday ⁡ x
10 9 uneq1d ⊢ p = x → bday ⁡ p ∪ bday ⁡ q = bday ⁡ x ∪ bday ⁡ q
11 10 eqeq2d ⊢ p = x → b = bday ⁡ p ∪ bday ⁡ q ↔ b = bday ⁡ x ∪ bday ⁡ q
12 fveq2 ⊢ p = x → + s ⁡ p = + s ⁡ x
13 12 eleq1d ⊢ p = x → + s ⁡ p ∈ No ↔ + s ⁡ x ∈ No
14 breq1 ⊢ p = x → p < s q ↔ x < s q
15 12 breq2d ⊢ p = x → + s ⁡ q < s + s ⁡ p ↔ + s ⁡ q < s + s ⁡ x
16 14 15 imbi12d ⊢ p = x → p < s q → + s ⁡ q < s + s ⁡ p ↔ x < s q → + s ⁡ q < s + s ⁡ x
17 13 16 anbi12d ⊢ p = x → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ + s ⁡ x ∈ No ∧ x < s q → + s ⁡ q < s + s ⁡ x
18 11 17 imbi12d ⊢ p = x → b = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ b = bday ⁡ x ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s q → + s ⁡ q < s + s ⁡ x
19 fveq2 ⊢ q = y → bday ⁡ q = bday ⁡ y
20 19 uneq2d ⊢ q = y → bday ⁡ x ∪ bday ⁡ q = bday ⁡ x ∪ bday ⁡ y
21 20 eqeq2d ⊢ q = y → b = bday ⁡ x ∪ bday ⁡ q ↔ b = bday ⁡ x ∪ bday ⁡ y
22 breq2 ⊢ q = y → x < s q ↔ x < s y
23 fveq2 ⊢ q = y → + s ⁡ q = + s ⁡ y
24 23 breq1d ⊢ q = y → + s ⁡ q < s + s ⁡ x ↔ + s ⁡ y < s + s ⁡ x
25 22 24 imbi12d ⊢ q = y → x < s q → + s ⁡ q < s + s ⁡ x ↔ x < s y → + s ⁡ y < s + s ⁡ x
26 25 anbi2d ⊢ q = y → + s ⁡ x ∈ No ∧ x < s q → + s ⁡ q < s + s ⁡ x ↔ + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
27 21 26 imbi12d ⊢ q = y → b = bday ⁡ x ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s q → + s ⁡ q < s + s ⁡ x ↔ b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
28 18 27 cbvral2vw ⊢ ∀ p ∈ No ∀ q ∈ No b = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
29 8 28 bitrdi ⊢ a = b → ∀ p ∈ No ∀ q ∈ No a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
30 raleq ⊢ a = bday ⁡ p ∪ bday ⁡ q → ∀ b ∈ a ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∀ b ∈ bday ⁡ p ∪ bday ⁡ q ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
31 ralrot3 ⊢ ∀ x ∈ No ∀ y ∈ No ∀ b ∈ bday ⁡ p ∪ bday ⁡ q b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∀ b ∈ bday ⁡ p ∪ bday ⁡ q ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
32 r19.23v ⊢ ∀ b ∈ bday ⁡ p ∪ bday ⁡ q b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∃ b ∈ bday ⁡ p ∪ bday ⁡ q b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
33 risset ⊢ bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q ↔ ∃ b ∈ bday ⁡ p ∪ bday ⁡ q b = bday ⁡ x ∪ bday ⁡ y
34 33 imbi1i ⊢ bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∃ b ∈ bday ⁡ p ∪ bday ⁡ q b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
35 32 34 bitr4i ⊢ ∀ b ∈ bday ⁡ p ∪ bday ⁡ q b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
36 35 2ralbii ⊢ ∀ x ∈ No ∀ y ∈ No ∀ b ∈ bday ⁡ p ∪ bday ⁡ q b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
37 31 36 bitr3i ⊢ ∀ b ∈ bday ⁡ p ∪ bday ⁡ q ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
38 30 37 bitrdi ⊢ a = bday ⁡ p ∪ bday ⁡ q → ∀ b ∈ a ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ↔ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
39 simpr ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
40 simpll ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → p ∈ No
41 39 40 negsproplem3 ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → + s ⁡ p ∈ No ∧ + s R ⁡ p ≪ s + s ⁡ p ∧ + s ⁡ p ≪ s + s L ⁡ p
42 41 simp1d ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → + s ⁡ p ∈ No
43 simplr ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ∧ p < s q → ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x
44 simplll ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ∧ p < s q → p ∈ No
45 simpllr ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ∧ p < s q → q ∈ No
46 simpr ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ∧ p < s q → p < s q
47 43 44 45 46 negsproplem7 ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x ∧ p < s q → + s ⁡ q < s + s ⁡ p
48 47 ex ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → p < s q → + s ⁡ q < s + s ⁡ p
49 42 48 jca ⊢ p ∈ No ∧ q ∈ No ∧ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
50 49 expcom ⊢ ∀ x ∈ No ∀ y ∈ No bday ⁡ x ∪ bday ⁡ y ∈ bday ⁡ p ∪ bday ⁡ q → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → p ∈ No ∧ q ∈ No → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
51 38 50 biimtrdi ⊢ a = bday ⁡ p ∪ bday ⁡ q → ∀ b ∈ a ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → p ∈ No ∧ q ∈ No → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
52 51 com3l ⊢ ∀ b ∈ a ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → p ∈ No ∧ q ∈ No → a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
53 52 ralrimivv ⊢ ∀ b ∈ a ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → ∀ p ∈ No ∀ q ∈ No a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
54 53 a1i ⊢ a ∈ On → ∀ b ∈ a ∀ x ∈ No ∀ y ∈ No b = bday ⁡ x ∪ bday ⁡ y → + s ⁡ x ∈ No ∧ x < s y → + s ⁡ y < s + s ⁡ x → ∀ p ∈ No ∀ q ∈ No a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
55 29 54 tfis2 ⊢ a ∈ On → ∀ p ∈ No ∀ q ∈ No a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p
56 fveq2 ⊢ p = A → bday ⁡ p = bday ⁡ A
57 56 uneq1d ⊢ p = A → bday ⁡ p ∪ bday ⁡ q = bday ⁡ A ∪ bday ⁡ q
58 57 eqeq2d ⊢ p = A → a = bday ⁡ p ∪ bday ⁡ q ↔ a = bday ⁡ A ∪ bday ⁡ q
59 fveq2 ⊢ p = A → + s ⁡ p = + s ⁡ A
60 59 eleq1d ⊢ p = A → + s ⁡ p ∈ No ↔ + s ⁡ A ∈ No
61 breq1 ⊢ p = A → p < s q ↔ A < s q
62 59 breq2d ⊢ p = A → + s ⁡ q < s + s ⁡ p ↔ + s ⁡ q < s + s ⁡ A
63 61 62 imbi12d ⊢ p = A → p < s q → + s ⁡ q < s + s ⁡ p ↔ A < s q → + s ⁡ q < s + s ⁡ A
64 60 63 anbi12d ⊢ p = A → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ + s ⁡ A ∈ No ∧ A < s q → + s ⁡ q < s + s ⁡ A
65 58 64 imbi12d ⊢ p = A → a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p ↔ a = bday ⁡ A ∪ bday ⁡ q → + s ⁡ A ∈ No ∧ A < s q → + s ⁡ q < s + s ⁡ A
66 fveq2 ⊢ q = B → bday ⁡ q = bday ⁡ B
67 66 uneq2d ⊢ q = B → bday ⁡ A ∪ bday ⁡ q = bday ⁡ A ∪ bday ⁡ B
68 67 eqeq2d ⊢ q = B → a = bday ⁡ A ∪ bday ⁡ q ↔ a = bday ⁡ A ∪ bday ⁡ B
69 breq2 ⊢ q = B → A < s q ↔ A < s B
70 fveq2 ⊢ q = B → + s ⁡ q = + s ⁡ B
71 70 breq1d ⊢ q = B → + s ⁡ q < s + s ⁡ A ↔ + s ⁡ B < s + s ⁡ A
72 69 71 imbi12d ⊢ q = B → A < s q → + s ⁡ q < s + s ⁡ A ↔ A < s B → + s ⁡ B < s + s ⁡ A
73 72 anbi2d ⊢ q = B → + s ⁡ A ∈ No ∧ A < s q → + s ⁡ q < s + s ⁡ A ↔ + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A
74 68 73 imbi12d ⊢ q = B → a = bday ⁡ A ∪ bday ⁡ q → + s ⁡ A ∈ No ∧ A < s q → + s ⁡ q < s + s ⁡ A ↔ a = bday ⁡ A ∪ bday ⁡ B → + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A
75 65 74 rspc2v ⊢ A ∈ No ∧ B ∈ No → ∀ p ∈ No ∀ q ∈ No a = bday ⁡ p ∪ bday ⁡ q → + s ⁡ p ∈ No ∧ p < s q → + s ⁡ q < s + s ⁡ p → a = bday ⁡ A ∪ bday ⁡ B → + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A
76 55 75 syl5com ⊢ a ∈ On → A ∈ No ∧ B ∈ No → a = bday ⁡ A ∪ bday ⁡ B → + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A
77 76 com23 ⊢ a ∈ On → a = bday ⁡ A ∪ bday ⁡ B → A ∈ No ∧ B ∈ No → + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A
78 77 rexlimiv ⊢ ∃ a ∈ On a = bday ⁡ A ∪ bday ⁡ B → A ∈ No ∧ B ∈ No → + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A
79 5 78 ax-mp ⊢ A ∈ No ∧ B ∈ No → + s ⁡ A ∈ No ∧ A < s B → + s ⁡ B < s + s ⁡ A