Metamath Proof Explorer

Theorem readdscl

Description: The surreal reals are closed under addition. Part of theorem 13(ii) of Conway p. 24. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion readdscl ( ( 𝐴 ∈ ℝs ∧ 𝐵 ∈ ℝs ) → ( 𝐴 +s 𝐵 ) ∈ ℝs )

Proof

Step Hyp Ref Expression
1 addscl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) ∈ No )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) ) → ( 𝐴 +s 𝐵 ) ∈ No )
3 nnaddscl ⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝑛 +s 𝑚 ) ∈ ℕs )
4 3 adantr ⊢ ( ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) → ( 𝑛 +s 𝑚 ) ∈ ℕs )
5 4 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( 𝑛 +s 𝑚 ) ∈ ℕs )
6 simprll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝑛 ∈ ℕs )
7 6 nnnod ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝑛 ∈ No )
8 simprlr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝑚 ∈ ℕs )
9 8 nnnod ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝑚 ∈ No )
10 negsdi ⊢ ( ( 𝑛 ∈ No ∧ 𝑚 ∈ No ) → ( -us ‘ ( 𝑛 +s 𝑚 ) ) = ( ( -us ‘ 𝑛 ) +s ( -us ‘ 𝑚 ) ) )
11 7 9 10 syl2anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( -us ‘ ( 𝑛 +s 𝑚 ) ) = ( ( -us ‘ 𝑛 ) +s ( -us ‘ 𝑚 ) ) )
12 7 negscld ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( -us ‘ 𝑛 ) ∈ No )
13 9 negscld ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( -us ‘ 𝑚 ) ∈ No )
14 simpll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝐴 ∈ No )
15 simplr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝐵 ∈ No )
16 simprll ⊢ ( ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) → ( -us ‘ 𝑛 ) <s 𝐴 )
17 16 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( -us ‘ 𝑛 ) <s 𝐴 )
18 simprrl ⊢ ( ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) → ( -us ‘ 𝑚 ) <s 𝐵 )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( -us ‘ 𝑚 ) <s 𝐵 )
20 12 13 14 15 17 19 lt2addsd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( ( -us ‘ 𝑛 ) +s ( -us ‘ 𝑚 ) ) <s ( 𝐴 +s 𝐵 ) )
21 11 20 eqbrtrd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( -us ‘ ( 𝑛 +s 𝑚 ) ) <s ( 𝐴 +s 𝐵 ) )
22 simprlr ⊢ ( ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) → 𝐴 <s 𝑛 )
23 22 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝐴 <s 𝑛 )
24 simprrr ⊢ ( ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) → 𝐵 <s 𝑚 )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → 𝐵 <s 𝑚 )
26 14 15 7 9 23 25 lt2addsd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ( 𝐴 +s 𝐵 ) <s ( 𝑛 +s 𝑚 ) )
27 fveq2 ⊢ ( 𝑝 = ( 𝑛 +s 𝑚 ) → ( -us ‘ 𝑝 ) = ( -us ‘ ( 𝑛 +s 𝑚 ) ) )
28 27 breq1d ⊢ ( 𝑝 = ( 𝑛 +s 𝑚 ) → ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ↔ ( -us ‘ ( 𝑛 +s 𝑚 ) ) <s ( 𝐴 +s 𝐵 ) ) )
29 breq2 ⊢ ( 𝑝 = ( 𝑛 +s 𝑚 ) → ( ( 𝐴 +s 𝐵 ) <s 𝑝 ↔ ( 𝐴 +s 𝐵 ) <s ( 𝑛 +s 𝑚 ) ) )
30 28 29 anbi12d ⊢ ( 𝑝 = ( 𝑛 +s 𝑚 ) → ( ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) ↔ ( ( -us ‘ ( 𝑛 +s 𝑚 ) ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s ( 𝑛 +s 𝑚 ) ) ) )
31 30 rspcev ⊢ ( ( ( 𝑛 +s 𝑚 ) ∈ ℕs ∧ ( ( -us ‘ ( 𝑛 +s 𝑚 ) ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s ( 𝑛 +s 𝑚 ) ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) )
32 5 21 26 31 syl12anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) )
33 32 expr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) ) )
34 33 rexlimdvva ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) ) )
35 simpl ⊢ ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) → ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) )
36 simpl ⊢ ( ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) → ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) )
37 35 36 anim12i ⊢ ( ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) )
38 reeanv ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) ↔ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) )
39 37 38 sylibr ⊢ ( ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ) )
40 34 39 impel ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) )
41 simpr ⊢ ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) → 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) )
42 simpr ⊢ ( ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) → 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) )
43 41 42 anim12i ⊢ ( ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) )
44 simpll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → 𝐴 ∈ No )
45 recut ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } )
46 44 45 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } )
47 simplr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → 𝐵 ∈ No )
48 recut ⊢ ( 𝐵 ∈ No → { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } <<s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } )
49 47 48 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } <<s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } )
50 simprl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) )
51 simprr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) )
52 46 49 50 51 addsunif ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) |s ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) ) )
53 ovex ⊢ ( 𝐴 -s ( 1s /su 𝑛 ) ) ∈ V
54 oveq1 ⊢ ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) → ( 𝑡 +s 𝐵 ) = ( ( 𝐴 -s ( 1s /su 𝑛 ) ) +s 𝐵 ) )
55 54 eqeq2d ⊢ ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) → ( 𝑧 = ( 𝑡 +s 𝐵 ) ↔ 𝑧 = ( ( 𝐴 -s ( 1s /su 𝑛 ) ) +s 𝐵 ) ) )
56 53 55 ceqsexv ⊢ ( ∃ 𝑡 ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ 𝑧 = ( ( 𝐴 -s ( 1s /su 𝑛 ) ) +s 𝐵 ) )
57 simpll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → 𝐴 ∈ No )
58 simplr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → 𝐵 ∈ No )
59 1no ⊢ 1s ∈ No
60 59 a1i ⊢ ( 𝑛 ∈ ℕs → 1s ∈ No )
61 nnno ⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ No )
62 nnne0s ⊢ ( 𝑛 ∈ ℕs → 𝑛 ≠ 0s )
63 60 61 62 divscld ⊢ ( 𝑛 ∈ ℕs → ( 1s /su 𝑛 ) ∈ No )
64 63 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → ( 1s /su 𝑛 ) ∈ No )
65 57 58 64 addsubsd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑛 ) ) = ( ( 𝐴 -s ( 1s /su 𝑛 ) ) +s 𝐵 ) )
66 65 eqeq2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → ( 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑛 ) ) ↔ 𝑧 = ( ( 𝐴 -s ( 1s /su 𝑛 ) ) +s 𝐵 ) ) )
67 56 66 bitr4id ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → ( ∃ 𝑡 ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑛 ) ) ) )
68 67 rexbidva ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑛 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑛 ) ) ) )
69 r19.41v ⊢ ( ∃ 𝑛 ∈ ℕs ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ( ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
70 69 exbii ⊢ ( ∃ 𝑡 ∃ 𝑛 ∈ ℕs ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ∃ 𝑡 ( ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
71 rexcom4 ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ∃ 𝑡 ∃ 𝑛 ∈ ℕs ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
72 eqeq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ↔ 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
73 72 rexbidv ⊢ ( 𝑥 = 𝑡 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
74 73 rexab ⊢ ( ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) ↔ ∃ 𝑡 ( ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
75 70 71 74 3bitr4ri ⊢ ( ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
76 oveq2 ⊢ ( 𝑝 = 𝑛 → ( 1s /su 𝑝 ) = ( 1s /su 𝑛 ) )
77 76 oveq2d ⊢ ( 𝑝 = 𝑛 → ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑛 ) ) )
78 77 eqeq2d ⊢ ( 𝑝 = 𝑛 → ( 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑛 ) ) ) )
79 78 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑛 ) ) )
80 68 75 79 3bitr4g ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) ↔ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) ) )
81 80 abbidv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } )
82 ovex ⊢ ( 𝐵 -s ( 1s /su 𝑚 ) ) ∈ V
83 oveq2 ⊢ ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) → ( 𝐴 +s 𝑡 ) = ( 𝐴 +s ( 𝐵 -s ( 1s /su 𝑚 ) ) ) )
84 83 eqeq2d ⊢ ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) → ( 𝑧 = ( 𝐴 +s 𝑡 ) ↔ 𝑧 = ( 𝐴 +s ( 𝐵 -s ( 1s /su 𝑚 ) ) ) ) )
85 82 84 ceqsexv ⊢ ( ∃ 𝑡 ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ 𝑧 = ( 𝐴 +s ( 𝐵 -s ( 1s /su 𝑚 ) ) ) )
86 simpll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → 𝐴 ∈ No )
87 simplr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → 𝐵 ∈ No )
88 59 a1i ⊢ ( 𝑚 ∈ ℕs → 1s ∈ No )
89 nnno ⊢ ( 𝑚 ∈ ℕs → 𝑚 ∈ No )
90 nnne0s ⊢ ( 𝑚 ∈ ℕs → 𝑚 ≠ 0s )
91 88 89 90 divscld ⊢ ( 𝑚 ∈ ℕs → ( 1s /su 𝑚 ) ∈ No )
92 91 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → ( 1s /su 𝑚 ) ∈ No )
93 86 87 92 addsubsassd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑚 ) ) = ( 𝐴 +s ( 𝐵 -s ( 1s /su 𝑚 ) ) ) )
94 93 eqeq2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → ( 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑚 ) ) ↔ 𝑧 = ( 𝐴 +s ( 𝐵 -s ( 1s /su 𝑚 ) ) ) ) )
95 85 94 bitr4id ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → ( ∃ 𝑡 ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑚 ) ) ) )
96 95 rexbidva ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑚 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑚 ) ) ) )
97 r19.41v ⊢ ( ∃ 𝑚 ∈ ℕs ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ( ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
98 97 exbii ⊢ ( ∃ 𝑡 ∃ 𝑚 ∈ ℕs ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ∃ 𝑡 ( ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
99 rexcom4 ⊢ ( ∃ 𝑚 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ∃ 𝑡 ∃ 𝑚 ∈ ℕs ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
100 eqeq1 ⊢ ( 𝑦 = 𝑡 → ( 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ↔ 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ) )
101 100 rexbidv ⊢ ( 𝑦 = 𝑡 → ( ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ) )
102 101 rexab ⊢ ( ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) ↔ ∃ 𝑡 ( ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
103 98 99 102 3bitr4ri ⊢ ( ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) ↔ ∃ 𝑚 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐵 -s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
104 oveq2 ⊢ ( 𝑝 = 𝑚 → ( 1s /su 𝑝 ) = ( 1s /su 𝑚 ) )
105 104 oveq2d ⊢ ( 𝑝 = 𝑚 → ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑚 ) ) )
106 105 eqeq2d ⊢ ( 𝑝 = 𝑚 → ( 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑚 ) ) ) )
107 106 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑚 ) ) )
108 96 103 107 3bitr4g ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) ↔ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) ) )
109 108 abbidv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } )
110 81 109 uneq12d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } ∪ { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } ) )
111 unidm ⊢ ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } ∪ { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } ) = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) }
112 110 111 eqtrdi ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } )
113 ovex ⊢ ( 𝐴 +s ( 1s /su 𝑛 ) ) ∈ V
114 oveq1 ⊢ ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) → ( 𝑡 +s 𝐵 ) = ( ( 𝐴 +s ( 1s /su 𝑛 ) ) +s 𝐵 ) )
115 114 eqeq2d ⊢ ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) → ( 𝑧 = ( 𝑡 +s 𝐵 ) ↔ 𝑧 = ( ( 𝐴 +s ( 1s /su 𝑛 ) ) +s 𝐵 ) ) )
116 113 115 ceqsexv ⊢ ( ∃ 𝑡 ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ 𝑧 = ( ( 𝐴 +s ( 1s /su 𝑛 ) ) +s 𝐵 ) )
117 57 64 58 adds32d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → ( ( 𝐴 +s ( 1s /su 𝑛 ) ) +s 𝐵 ) = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑛 ) ) )
118 117 eqeq2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → ( 𝑧 = ( ( 𝐴 +s ( 1s /su 𝑛 ) ) +s 𝐵 ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑛 ) ) ) )
119 116 118 bitrid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑛 ∈ ℕs ) → ( ∃ 𝑡 ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑛 ) ) ) )
120 119 rexbidva ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑛 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑛 ) ) ) )
121 r19.41v ⊢ ( ∃ 𝑛 ∈ ℕs ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ( ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
122 121 exbii ⊢ ( ∃ 𝑡 ∃ 𝑛 ∈ ℕs ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ∃ 𝑡 ( ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
123 rexcom4 ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) ↔ ∃ 𝑡 ∃ 𝑛 ∈ ℕs ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
124 eqeq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
125 124 rexbidv ⊢ ( 𝑥 = 𝑡 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
126 125 rexab ⊢ ( ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) ↔ ∃ 𝑡 ( ∃ 𝑛 ∈ ℕs 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
127 122 123 126 3bitr4ri ⊢ ( ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝑡 +s 𝐵 ) ) )
128 76 oveq2d ⊢ ( 𝑝 = 𝑛 → ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑛 ) ) )
129 128 eqeq2d ⊢ ( 𝑝 = 𝑛 → ( 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑛 ) ) ) )
130 129 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑛 ) ) )
131 120 127 130 3bitr4g ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) ↔ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) ) )
132 131 abbidv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } )
133 ovex ⊢ ( 𝐵 +s ( 1s /su 𝑚 ) ) ∈ V
134 oveq2 ⊢ ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) → ( 𝐴 +s 𝑡 ) = ( 𝐴 +s ( 𝐵 +s ( 1s /su 𝑚 ) ) ) )
135 134 eqeq2d ⊢ ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) → ( 𝑧 = ( 𝐴 +s 𝑡 ) ↔ 𝑧 = ( 𝐴 +s ( 𝐵 +s ( 1s /su 𝑚 ) ) ) ) )
136 133 135 ceqsexv ⊢ ( ∃ 𝑡 ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ 𝑧 = ( 𝐴 +s ( 𝐵 +s ( 1s /su 𝑚 ) ) ) )
137 86 87 92 addsassd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑚 ) ) = ( 𝐴 +s ( 𝐵 +s ( 1s /su 𝑚 ) ) ) )
138 137 eqeq2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → ( 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑚 ) ) ↔ 𝑧 = ( 𝐴 +s ( 𝐵 +s ( 1s /su 𝑚 ) ) ) ) )
139 136 138 bitr4id ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑚 ∈ ℕs ) → ( ∃ 𝑡 ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑚 ) ) ) )
140 139 rexbidva ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑚 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑚 ) ) ) )
141 r19.41v ⊢ ( ∃ 𝑚 ∈ ℕs ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ( ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
142 141 exbii ⊢ ( ∃ 𝑡 ∃ 𝑚 ∈ ℕs ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ∃ 𝑡 ( ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
143 rexcom4 ⊢ ( ∃ 𝑚 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) ↔ ∃ 𝑡 ∃ 𝑚 ∈ ℕs ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
144 eqeq1 ⊢ ( 𝑦 = 𝑡 → ( 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ↔ 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ) )
145 144 rexbidv ⊢ ( 𝑦 = 𝑡 → ( ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ) )
146 145 rexab ⊢ ( ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) ↔ ∃ 𝑡 ( ∃ 𝑚 ∈ ℕs 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
147 142 143 146 3bitr4ri ⊢ ( ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) ↔ ∃ 𝑚 ∈ ℕs ∃ 𝑡 ( 𝑡 = ( 𝐵 +s ( 1s /su 𝑚 ) ) ∧ 𝑧 = ( 𝐴 +s 𝑡 ) ) )
148 104 oveq2d ⊢ ( 𝑝 = 𝑚 → ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑚 ) ) )
149 148 eqeq2d ⊢ ( 𝑝 = 𝑚 → ( 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) ↔ 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑚 ) ) ) )
150 149 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑚 ) ) )
151 140 147 150 3bitr4g ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) ↔ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) ) )
152 151 abbidv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } )
153 132 152 uneq12d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ∪ { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) )
154 unidm ⊢ ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ∪ { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) }
155 153 154 eqtrdi ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) = { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } )
156 112 155 oveq12d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) |s ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } |s { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) )
157 156 adantr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → ( ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) |s ( { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } 𝑧 = ( 𝑡 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑡 ∈ { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } 𝑧 = ( 𝐴 +s 𝑡 ) } ) ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } |s { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) )
158 52 157 eqtrd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) → ( 𝐴 +s 𝐵 ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } |s { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) )
159 43 158 sylan2 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) ) → ( 𝐴 +s 𝐵 ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } |s { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) )
160 2 40 159 jca32 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) ) → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) ∧ ( 𝐴 +s 𝐵 ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } |s { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) ) ) )
161 160 an4s ⊢ ( ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) ∧ ( 𝐵 ∈ No ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) ) → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) ∧ ( 𝐴 +s 𝐵 ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } |s { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) ) ) )
162 elreno ⊢ ( 𝐴 ∈ ℝs ↔ ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) )
163 elreno ⊢ ( 𝐵 ∈ ℝs ↔ ( 𝐵 ∈ No ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) )
164 162 163 anbi12i ⊢ ( ( 𝐴 ∈ ℝs ∧ 𝐵 ∈ ℝs ) ↔ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) ∧ ( 𝐵 ∈ No ∧ ( ∃ 𝑚 ∈ ℕs ( ( -us ‘ 𝑚 ) <s 𝐵 ∧ 𝐵 <s 𝑚 ) ∧ 𝐵 = ( { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 -s ( 1s /su 𝑚 ) ) } |s { 𝑦 ∣ ∃ 𝑚 ∈ ℕs 𝑦 = ( 𝐵 +s ( 1s /su 𝑚 ) ) } ) ) ) ) )
165 elreno ⊢ ( ( 𝐴 +s 𝐵 ) ∈ ℝs ↔ ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 +s 𝐵 ) ∧ ( 𝐴 +s 𝐵 ) <s 𝑝 ) ∧ ( 𝐴 +s 𝐵 ) = ( { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) -s ( 1s /su 𝑝 ) ) } |s { 𝑧 ∣ ∃ 𝑝 ∈ ℕs 𝑧 = ( ( 𝐴 +s 𝐵 ) +s ( 1s /su 𝑝 ) ) } ) ) ) )
166 161 164 165 3imtr4i ⊢ ( ( 𝐴 ∈ ℝs ∧ 𝐵 ∈ ℝs ) → ( 𝐴 +s 𝐵 ) ∈ ℝs )