Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  negsid Structured version   Visualization version   GIF version

Theorem negsid 34327
Description: Surreal addition of a number and its negative. Theorem 4(iii) of [Conway] p. 17. (Contributed by Scott Fenton, 3-Feb-2025.)
Assertion
Ref Expression
negsid (𝐴 No → (𝐴 +s ( -us ‘𝐴)) = 0s )

Proof of Theorem negsid
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑥 𝑥L 𝑥R 𝑥O are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . 4 (𝑥 = 𝑥O𝑥 = 𝑥O)
2 fveq2 6839 . . . 4 (𝑥 = 𝑥O → ( -us ‘𝑥) = ( -us ‘𝑥O))
31, 2oveq12d 7369 . . 3 (𝑥 = 𝑥O → (𝑥 +s ( -us ‘𝑥)) = (𝑥O +s ( -us ‘𝑥O)))
43eqeq1d 2739 . 2 (𝑥 = 𝑥O → ((𝑥 +s ( -us ‘𝑥)) = 0s ↔ (𝑥O +s ( -us ‘𝑥O)) = 0s ))
5 id 22 . . . 4 (𝑥 = 𝐴𝑥 = 𝐴)
6 fveq2 6839 . . . 4 (𝑥 = 𝐴 → ( -us ‘𝑥) = ( -us ‘𝐴))
75, 6oveq12d 7369 . . 3 (𝑥 = 𝐴 → (𝑥 +s ( -us ‘𝑥)) = (𝐴 +s ( -us ‘𝐴)))
87eqeq1d 2739 . 2 (𝑥 = 𝐴 → ((𝑥 +s ( -us ‘𝑥)) = 0s ↔ (𝐴 +s ( -us ‘𝐴)) = 0s ))
9 lltropt 27153 . . . . . 6 (𝑥 No → ( L ‘𝑥) <<s ( R ‘𝑥))
109adantr 481 . . . . 5 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ( L ‘𝑥) <<s ( R ‘𝑥))
11 negscut2 34326 . . . . . 6 (𝑥 No → ( -us “ ( R ‘𝑥)) <<s ( -us “ ( L ‘𝑥)))
1211adantr 481 . . . . 5 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ( -us “ ( R ‘𝑥)) <<s ( -us “ ( L ‘𝑥)))
13 lrcut 27180 . . . . . . 7 (𝑥 No → (( L ‘𝑥) |s ( R ‘𝑥)) = 𝑥)
1413adantr 481 . . . . . 6 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (( L ‘𝑥) |s ( R ‘𝑥)) = 𝑥)
1514eqcomd 2743 . . . . 5 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → 𝑥 = (( L ‘𝑥) |s ( R ‘𝑥)))
16 negsval 34312 . . . . . 6 (𝑥 No → ( -us ‘𝑥) = (( -us “ ( R ‘𝑥)) |s ( -us “ ( L ‘𝑥))))
1716adantr 481 . . . . 5 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ( -us ‘𝑥) = (( -us “ ( R ‘𝑥)) |s ( -us “ ( L ‘𝑥))))
1810, 12, 15, 17addsunif 34300 . . . 4 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (𝑥 +s ( -us ‘𝑥)) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)})))
19 negsfn 34310 . . . . . . . . 9 -us Fn No
20 rightssno 27161 . . . . . . . . 9 ( R ‘𝑥) ⊆ No
21 oveq2 7359 . . . . . . . . . . 11 (𝑝 = ( -us ‘𝑥R) → (𝑥 +s 𝑝) = (𝑥 +s ( -us ‘𝑥R)))
2221eqeq2d 2748 . . . . . . . . . 10 (𝑝 = ( -us ‘𝑥R) → (𝑏 = (𝑥 +s 𝑝) ↔ 𝑏 = (𝑥 +s ( -us ‘𝑥R))))
2322imaeqsexv 34104 . . . . . . . . 9 (( -us Fn No ∧ ( R ‘𝑥) ⊆ No ) → (∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))))
2419, 20, 23mp2an 690 . . . . . . . 8 (∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R)))
2524abbii 2807 . . . . . . 7 {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)} = {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}
2625uneq2i 4118 . . . . . 6 ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) = ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))})
27 leftssno 27160 . . . . . . . . 9 ( L ‘𝑥) ⊆ No
28 oveq2 7359 . . . . . . . . . . 11 (𝑞 = ( -us ‘𝑥L) → (𝑥 +s 𝑞) = (𝑥 +s ( -us ‘𝑥L)))
2928eqeq2d 2748 . . . . . . . . . 10 (𝑞 = ( -us ‘𝑥L) → (𝑑 = (𝑥 +s 𝑞) ↔ 𝑑 = (𝑥 +s ( -us ‘𝑥L))))
3029imaeqsexv 34104 . . . . . . . . 9 (( -us Fn No ∧ ( L ‘𝑥) ⊆ No ) → (∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))))
3119, 27, 30mp2an 690 . . . . . . . 8 (∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L)))
3231abbii 2807 . . . . . . 7 {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)} = {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}
3332uneq2i 4118 . . . . . 6 ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)}) = ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})
3426, 33oveq12i 7363 . . . . 5 (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)})) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}))
35 fvex 6852 . . . . . . . . . 10 ( L ‘𝑥) ∈ V
3635abrexex 7887 . . . . . . . . 9 {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∈ V
37 fvex 6852 . . . . . . . . . 10 ( R ‘𝑥) ∈ V
3837abrexex 7887 . . . . . . . . 9 {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))} ∈ V
3936, 38unex 7672 . . . . . . . 8 ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∈ V
4039a1i 11 . . . . . . 7 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∈ V)
41 snex 5386 . . . . . . . 8 { 0s } ∈ V
4241a1i 11 . . . . . . 7 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → { 0s } ∈ V)
4327sseli 3938 . . . . . . . . . . . . 13 (𝑥L ∈ ( L ‘𝑥) → 𝑥L No )
4443adantl 482 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → 𝑥L No )
45 simpll 765 . . . . . . . . . . . . 13 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → 𝑥 No )
4645negscld 34323 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → ( -us ‘𝑥) ∈ No )
4744, 46addscld 34286 . . . . . . . . . . 11 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥L +s ( -us ‘𝑥)) ∈ No )
48 eleq1 2825 . . . . . . . . . . 11 (𝑎 = (𝑥L +s ( -us ‘𝑥)) → (𝑎 No ↔ (𝑥L +s ( -us ‘𝑥)) ∈ No ))
4947, 48syl5ibrcom 246 . . . . . . . . . 10 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑎 = (𝑥L +s ( -us ‘𝑥)) → 𝑎 No ))
5049rexlimdva 3150 . . . . . . . . 9 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥)) → 𝑎 No ))
5150abssdv 4023 . . . . . . . 8 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ⊆ No )
52 simpll 765 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → 𝑥 No )
5320sseli 3938 . . . . . . . . . . . . . 14 (𝑥R ∈ ( R ‘𝑥) → 𝑥R No )
5453adantl 482 . . . . . . . . . . . . 13 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → 𝑥R No )
5554negscld 34323 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → ( -us ‘𝑥R) ∈ No )
5652, 55addscld 34286 . . . . . . . . . . 11 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥 +s ( -us ‘𝑥R)) ∈ No )
57 eleq1 2825 . . . . . . . . . . 11 (𝑏 = (𝑥 +s ( -us ‘𝑥R)) → (𝑏 No ↔ (𝑥 +s ( -us ‘𝑥R)) ∈ No ))
5856, 57syl5ibrcom 246 . . . . . . . . . 10 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑏 = (𝑥 +s ( -us ‘𝑥R)) → 𝑏 No ))
5958rexlimdva 3150 . . . . . . . . 9 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R)) → 𝑏 No ))
6059abssdv 4023 . . . . . . . 8 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))} ⊆ No )
6151, 60unssd 4144 . . . . . . 7 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ⊆ No )
62 0sno 27116 . . . . . . . 8 0s ∈ No
63 snssi 4766 . . . . . . . 8 ( 0s ∈ No → { 0s } ⊆ No )
6462, 63mp1i 13 . . . . . . 7 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → { 0s } ⊆ No )
65 elun 4106 . . . . . . . . . . 11 (𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ↔ (𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∨ 𝑝 ∈ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}))
66 vex 3447 . . . . . . . . . . . . 13 𝑝 ∈ V
67 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑎 = 𝑝 → (𝑎 = (𝑥L +s ( -us ‘𝑥)) ↔ 𝑝 = (𝑥L +s ( -us ‘𝑥))))
6867rexbidv 3173 . . . . . . . . . . . . 13 (𝑎 = 𝑝 → (∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥)) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥))))
6966, 68elab 3628 . . . . . . . . . . . 12 (𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)))
70 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑏 = (𝑥 +s ( -us ‘𝑥R)) ↔ 𝑝 = (𝑥 +s ( -us ‘𝑥R))))
7170rexbidv 3173 . . . . . . . . . . . . 13 (𝑏 = 𝑝 → (∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R)) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))))
7266, 71elab 3628 . . . . . . . . . . . 12 (𝑝 ∈ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))} ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))
7369, 72orbi12i 913 . . . . . . . . . . 11 ((𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∨ 𝑝 ∈ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ↔ (∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))))
7465, 73bitri 274 . . . . . . . . . 10 (𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ↔ (∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))))
75 velsn 4600 . . . . . . . . . 10 (𝑞 ∈ { 0s } ↔ 𝑞 = 0s )
7674, 75anbi12i 627 . . . . . . . . 9 ((𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∧ 𝑞 ∈ { 0s }) ↔ ((∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))) ∧ 𝑞 = 0s ))
77 leftval 27144 . . . . . . . . . . . . . . . . . . . . 21 ( L ‘𝑥) = {𝑥L ∈ ( O ‘( bday 𝑥)) ∣ 𝑥L <s 𝑥}
7877rabeq2i 3427 . . . . . . . . . . . . . . . . . . . 20 (𝑥L ∈ ( L ‘𝑥) ↔ (𝑥L ∈ ( O ‘( bday 𝑥)) ∧ 𝑥L <s 𝑥))
7978simprbi 497 . . . . . . . . . . . . . . . . . . 19 (𝑥L ∈ ( L ‘𝑥) → 𝑥L <s 𝑥)
8079adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → 𝑥L <s 𝑥)
81 sltnegim 34324 . . . . . . . . . . . . . . . . . . 19 ((𝑥L No 𝑥 No ) → (𝑥L <s 𝑥 → ( -us ‘𝑥) <s ( -us ‘𝑥L)))
8244, 45, 81syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥L <s 𝑥 → ( -us ‘𝑥) <s ( -us ‘𝑥L)))
8380, 82mpd 15 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → ( -us ‘𝑥) <s ( -us ‘𝑥L))
8444negscld 34323 . . . . . . . . . . . . . . . . . 18 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → ( -us ‘𝑥L) ∈ No )
85 sltadd2 34296 . . . . . . . . . . . . . . . . . 18 ((( -us ‘𝑥) ∈ No ∧ ( -us ‘𝑥L) ∈ No 𝑥L No ) → (( -us ‘𝑥) <s ( -us ‘𝑥L) ↔ (𝑥L +s ( -us ‘𝑥)) <s (𝑥L +s ( -us ‘𝑥L))))
8646, 84, 44, 85syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (( -us ‘𝑥) <s ( -us ‘𝑥L) ↔ (𝑥L +s ( -us ‘𝑥)) <s (𝑥L +s ( -us ‘𝑥L))))
8783, 86mpbid 231 . . . . . . . . . . . . . . . 16 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥L +s ( -us ‘𝑥)) <s (𝑥L +s ( -us ‘𝑥L)))
88 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥O = 𝑥L𝑥O = 𝑥L)
89 fveq2 6839 . . . . . . . . . . . . . . . . . . 19 (𝑥O = 𝑥L → ( -us ‘𝑥O) = ( -us ‘𝑥L))
9088, 89oveq12d 7369 . . . . . . . . . . . . . . . . . 18 (𝑥O = 𝑥L → (𝑥O +s ( -us ‘𝑥O)) = (𝑥L +s ( -us ‘𝑥L)))
9190eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑥O = 𝑥L → ((𝑥O +s ( -us ‘𝑥O)) = 0s ↔ (𝑥L +s ( -us ‘𝑥L)) = 0s ))
92 simplr 767 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s )
93 elun1 4134 . . . . . . . . . . . . . . . . . 18 (𝑥L ∈ ( L ‘𝑥) → 𝑥L ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
9493adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → 𝑥L ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
9591, 92, 94rspcdva 3580 . . . . . . . . . . . . . . . 16 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥L +s ( -us ‘𝑥L)) = 0s )
9687, 95breqtrd 5129 . . . . . . . . . . . . . . 15 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥L +s ( -us ‘𝑥)) <s 0s )
97 breq1 5106 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥L +s ( -us ‘𝑥)) → (𝑝 <s 0s ↔ (𝑥L +s ( -us ‘𝑥)) <s 0s ))
9896, 97syl5ibrcom 246 . . . . . . . . . . . . . 14 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑝 = (𝑥L +s ( -us ‘𝑥)) → 𝑝 <s 0s ))
9998rexlimdva 3150 . . . . . . . . . . . . 13 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) → 𝑝 <s 0s ))
10099imp 407 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ ∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥))) → 𝑝 <s 0s )
101 rightval 27145 . . . . . . . . . . . . . . . . . . . 20 ( R ‘𝑥) = {𝑥R ∈ ( O ‘( bday 𝑥)) ∣ 𝑥 <s 𝑥R}
102101rabeq2i 3427 . . . . . . . . . . . . . . . . . . 19 (𝑥R ∈ ( R ‘𝑥) ↔ (𝑥R ∈ ( O ‘( bday 𝑥)) ∧ 𝑥 <s 𝑥R))
103102simprbi 497 . . . . . . . . . . . . . . . . . 18 (𝑥R ∈ ( R ‘𝑥) → 𝑥 <s 𝑥R)
104103adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → 𝑥 <s 𝑥R)
105 sltadd1 34297 . . . . . . . . . . . . . . . . . 18 ((𝑥 No 𝑥R No ∧ ( -us ‘𝑥R) ∈ No ) → (𝑥 <s 𝑥R ↔ (𝑥 +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us ‘𝑥R))))
10652, 54, 55, 105syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥 <s 𝑥R ↔ (𝑥 +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us ‘𝑥R))))
107104, 106mpbid 231 . . . . . . . . . . . . . . . 16 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥 +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us ‘𝑥R)))
108 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥O = 𝑥R𝑥O = 𝑥R)
109 fveq2 6839 . . . . . . . . . . . . . . . . . . 19 (𝑥O = 𝑥R → ( -us ‘𝑥O) = ( -us ‘𝑥R))
110108, 109oveq12d 7369 . . . . . . . . . . . . . . . . . 18 (𝑥O = 𝑥R → (𝑥O +s ( -us ‘𝑥O)) = (𝑥R +s ( -us ‘𝑥R)))
111110eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑥O = 𝑥R → ((𝑥O +s ( -us ‘𝑥O)) = 0s ↔ (𝑥R +s ( -us ‘𝑥R)) = 0s ))
112 simplr 767 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s )
113 elun2 4135 . . . . . . . . . . . . . . . . . 18 (𝑥R ∈ ( R ‘𝑥) → 𝑥R ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
114113adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → 𝑥R ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)))
115111, 112, 114rspcdva 3580 . . . . . . . . . . . . . . . 16 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥R +s ( -us ‘𝑥R)) = 0s )
116107, 115breqtrd 5129 . . . . . . . . . . . . . . 15 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥 +s ( -us ‘𝑥R)) <s 0s )
117 breq1 5106 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥 +s ( -us ‘𝑥R)) → (𝑝 <s 0s ↔ (𝑥 +s ( -us ‘𝑥R)) <s 0s ))
118116, 117syl5ibrcom 246 . . . . . . . . . . . . . 14 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑝 = (𝑥 +s ( -us ‘𝑥R)) → 𝑝 <s 0s ))
119118rexlimdva 3150 . . . . . . . . . . . . 13 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)) → 𝑝 <s 0s ))
120119imp 407 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))) → 𝑝 <s 0s )
121100, 120jaodan 956 . . . . . . . . . . 11 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ (∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))) → 𝑝 <s 0s )
122 breq2 5107 . . . . . . . . . . 11 (𝑞 = 0s → (𝑝 <s 𝑞𝑝 <s 0s ))
123121, 122syl5ibrcom 246 . . . . . . . . . 10 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ (∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R)))) → (𝑞 = 0s → 𝑝 <s 𝑞))
124123expimpd 454 . . . . . . . . 9 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (((∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s ( -us ‘𝑥)) ∨ ∃𝑥R ∈ ( R ‘𝑥)𝑝 = (𝑥 +s ( -us ‘𝑥R))) ∧ 𝑞 = 0s ) → 𝑝 <s 𝑞))
12576, 124biimtrid 241 . . . . . . . 8 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ((𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∧ 𝑞 ∈ { 0s }) → 𝑝 <s 𝑞))
1261253impib 1116 . . . . . . 7 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) ∧ 𝑞 ∈ { 0s }) → 𝑝 <s 𝑞)
12740, 42, 61, 64, 126ssltd 27082 . . . . . 6 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) <<s { 0s })
12837abrexex 7887 . . . . . . . . 9 {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∈ V
12935abrexex 7887 . . . . . . . . 9 {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))} ∈ V
130128, 129unex 7672 . . . . . . . 8 ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ∈ V
131130a1i 11 . . . . . . 7 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ∈ V)
13252negscld 34323 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → ( -us ‘𝑥) ∈ No )
13354, 132addscld 34286 . . . . . . . . . . 11 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥R +s ( -us ‘𝑥)) ∈ No )
134 eleq1 2825 . . . . . . . . . . 11 (𝑐 = (𝑥R +s ( -us ‘𝑥)) → (𝑐 No ↔ (𝑥R +s ( -us ‘𝑥)) ∈ No ))
135133, 134syl5ibrcom 246 . . . . . . . . . 10 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑐 = (𝑥R +s ( -us ‘𝑥)) → 𝑐 No ))
136135rexlimdva 3150 . . . . . . . . 9 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥)) → 𝑐 No ))
137136abssdv 4023 . . . . . . . 8 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ⊆ No )
13845, 84addscld 34286 . . . . . . . . . . 11 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥 +s ( -us ‘𝑥L)) ∈ No )
139 eleq1 2825 . . . . . . . . . . 11 (𝑑 = (𝑥 +s ( -us ‘𝑥L)) → (𝑑 No ↔ (𝑥 +s ( -us ‘𝑥L)) ∈ No ))
140138, 139syl5ibrcom 246 . . . . . . . . . 10 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑑 = (𝑥 +s ( -us ‘𝑥L)) → 𝑑 No ))
141140rexlimdva 3150 . . . . . . . . 9 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L)) → 𝑑 No ))
142141abssdv 4023 . . . . . . . 8 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))} ⊆ No )
143137, 142unssd 4144 . . . . . . 7 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ⊆ No )
144 velsn 4600 . . . . . . . . . 10 (𝑝 ∈ { 0s } ↔ 𝑝 = 0s )
145 elun 4106 . . . . . . . . . . 11 (𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ↔ (𝑞 ∈ {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∨ 𝑞 ∈ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}))
146 vex 3447 . . . . . . . . . . . . 13 𝑞 ∈ V
147 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐 = (𝑥R +s ( -us ‘𝑥)) ↔ 𝑞 = (𝑥R +s ( -us ‘𝑥))))
148147rexbidv 3173 . . . . . . . . . . . . 13 (𝑐 = 𝑞 → (∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥)) ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥))))
149146, 148elab 3628 . . . . . . . . . . . 12 (𝑞 ∈ {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ↔ ∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)))
150 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑑 = 𝑞 → (𝑑 = (𝑥 +s ( -us ‘𝑥L)) ↔ 𝑞 = (𝑥 +s ( -us ‘𝑥L))))
151150rexbidv 3173 . . . . . . . . . . . . 13 (𝑑 = 𝑞 → (∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L)) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))))
152146, 151elab 3628 . . . . . . . . . . . 12 (𝑞 ∈ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))} ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))
153149, 152orbi12i 913 . . . . . . . . . . 11 ((𝑞 ∈ {𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∨ 𝑞 ∈ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ↔ (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))))
154145, 153bitri 274 . . . . . . . . . 10 (𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}) ↔ (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))))
155144, 154anbi12i 627 . . . . . . . . 9 ((𝑝 ∈ { 0s } ∧ 𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) ↔ (𝑝 = 0s ∧ (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))))
156 sltnegim 34324 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 No 𝑥R No ) → (𝑥 <s 𝑥R → ( -us ‘𝑥R) <s ( -us ‘𝑥)))
15752, 54, 156syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥 <s 𝑥R → ( -us ‘𝑥R) <s ( -us ‘𝑥)))
158104, 157mpd 15 . . . . . . . . . . . . . . . . . 18 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → ( -us ‘𝑥R) <s ( -us ‘𝑥))
159 sltadd2 34296 . . . . . . . . . . . . . . . . . . 19 ((( -us ‘𝑥R) ∈ No ∧ ( -us ‘𝑥) ∈ No 𝑥R No ) → (( -us ‘𝑥R) <s ( -us ‘𝑥) ↔ (𝑥R +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us ‘𝑥))))
16055, 132, 54, 159syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (( -us ‘𝑥R) <s ( -us ‘𝑥) ↔ (𝑥R +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us ‘𝑥))))
161158, 160mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑥R +s ( -us ‘𝑥R)) <s (𝑥R +s ( -us ‘𝑥)))
162115, 161eqbrtrrd 5127 . . . . . . . . . . . . . . . 16 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → 0s <s (𝑥R +s ( -us ‘𝑥)))
163 breq2 5107 . . . . . . . . . . . . . . . 16 (𝑞 = (𝑥R +s ( -us ‘𝑥)) → ( 0s <s 𝑞 ↔ 0s <s (𝑥R +s ( -us ‘𝑥))))
164162, 163syl5ibrcom 246 . . . . . . . . . . . . . . 15 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥R ∈ ( R ‘𝑥)) → (𝑞 = (𝑥R +s ( -us ‘𝑥)) → 0s <s 𝑞))
165164rexlimdva 3150 . . . . . . . . . . . . . 14 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) → 0s <s 𝑞))
166165imp 407 . . . . . . . . . . . . 13 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ ∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥))) → 0s <s 𝑞)
167 sltadd1 34297 . . . . . . . . . . . . . . . . . . 19 ((𝑥L No 𝑥 No ∧ ( -us ‘𝑥L) ∈ No ) → (𝑥L <s 𝑥 ↔ (𝑥L +s ( -us ‘𝑥L)) <s (𝑥 +s ( -us ‘𝑥L))))
16844, 45, 84, 167syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥L <s 𝑥 ↔ (𝑥L +s ( -us ‘𝑥L)) <s (𝑥 +s ( -us ‘𝑥L))))
16980, 168mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑥L +s ( -us ‘𝑥L)) <s (𝑥 +s ( -us ‘𝑥L)))
17095, 169eqbrtrrd 5127 . . . . . . . . . . . . . . . 16 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → 0s <s (𝑥 +s ( -us ‘𝑥L)))
171 breq2 5107 . . . . . . . . . . . . . . . 16 (𝑞 = (𝑥 +s ( -us ‘𝑥L)) → ( 0s <s 𝑞 ↔ 0s <s (𝑥 +s ( -us ‘𝑥L))))
172170, 171syl5ibrcom 246 . . . . . . . . . . . . . . 15 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑥L ∈ ( L ‘𝑥)) → (𝑞 = (𝑥 +s ( -us ‘𝑥L)) → 0s <s 𝑞))
173172rexlimdva 3150 . . . . . . . . . . . . . 14 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)) → 0s <s 𝑞))
174173imp 407 . . . . . . . . . . . . 13 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))) → 0s <s 𝑞)
175166, 174jaodan 956 . . . . . . . . . . . 12 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) → 0s <s 𝑞)
176 breq1 5106 . . . . . . . . . . . 12 (𝑝 = 0s → (𝑝 <s 𝑞 ↔ 0s <s 𝑞))
177175, 176syl5ibrcom 246 . . . . . . . . . . 11 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) → (𝑝 = 0s → 𝑝 <s 𝑞))
178177ex 413 . . . . . . . . . 10 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ((∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L))) → (𝑝 = 0s → 𝑝 <s 𝑞)))
179178impcomd 412 . . . . . . . . 9 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ((𝑝 = 0s ∧ (∃𝑥R ∈ ( R ‘𝑥)𝑞 = (𝑥R +s ( -us ‘𝑥)) ∨ ∃𝑥L ∈ ( L ‘𝑥)𝑞 = (𝑥 +s ( -us ‘𝑥L)))) → 𝑝 <s 𝑞))
180155, 179biimtrid 241 . . . . . . . 8 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → ((𝑝 ∈ { 0s } ∧ 𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) → 𝑝 <s 𝑞))
1811803impib 1116 . . . . . . 7 (((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) ∧ 𝑝 ∈ { 0s } ∧ 𝑞 ∈ ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) → 𝑝 <s 𝑞)
18242, 131, 64, 143, 181ssltd 27082 . . . . . 6 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → { 0s } <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))}))
183127, 182cuteq0 27122 . . . . 5 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑏 = (𝑥 +s ( -us ‘𝑥R))}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑑 = (𝑥 +s ( -us ‘𝑥L))})) = 0s )
18434, 183eqtrid 2789 . . . 4 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s ( -us ‘𝑥))} ∪ {𝑏 ∣ ∃𝑝 ∈ ( -us “ ( R ‘𝑥))𝑏 = (𝑥 +s 𝑝)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s ( -us ‘𝑥))} ∪ {𝑑 ∣ ∃𝑞 ∈ ( -us “ ( L ‘𝑥))𝑑 = (𝑥 +s 𝑞)})) = 0s )
18518, 184eqtrd 2777 . . 3 ((𝑥 No ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s ) → (𝑥 +s ( -us ‘𝑥)) = 0s )
186185ex 413 . 2 (𝑥 No → (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥O +s ( -us ‘𝑥O)) = 0s → (𝑥 +s ( -us ‘𝑥)) = 0s ))
1874, 8, 186noinds 34253 1 (𝐴 No → (𝐴 +s ( -us ‘𝐴)) = 0s )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  {cab 2714  wral 3062  wrex 3071  Vcvv 3443  cun 3906  wss 3908  {csn 4584   class class class wbr 5103  cima 5634   Fn wfn 6488  cfv 6493  (class class class)co 7351   No csur 26939   <s cslt 26940   bday cbday 26941   <<s csslt 27071   |s cscut 27073   0s c0s 27112   O cold 27124   L cleft 27126   R cright 27127   +s cadds 34267   -us cnegs 34306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-1o 8404  df-2o 8405  df-no 26942  df-slt 26943  df-bday 26944  df-sle 27044  df-sslt 27072  df-scut 27074  df-0s 27114  df-made 27128  df-old 27129  df-left 27131  df-right 27132  df-nadd 34215  df-norec 34246  df-norec2 34257  df-adds 34268  df-negs 34308
This theorem is referenced by:  negsex  34328  negnegs  34329  subsid  34339  subadds  34340
  Copyright terms: Public domain W3C validator