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

Theorem addsunif 34336
Description: Uniformity theorem for surreal addition. This theorem states that we can use any cuts that define 𝐴 and 𝐵 in the definition of surreal addition. Theorem 3.2 of [Gonshor] p. 15. (Contributed by Scott Fenton, 21-Jan-2025.)
Hypotheses
Ref Expression
addsunif.1 (𝜑𝐿 <<s 𝑅)
addsunif.2 (𝜑𝑀 <<s 𝑆)
addsunif.3 (𝜑𝐴 = (𝐿 |s 𝑅))
addsunif.4 (𝜑𝐵 = (𝑀 |s 𝑆))
Assertion
Ref Expression
addsunif (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})))
Distinct variable groups:   𝐴,𝑟,𝑠,𝑙,𝑚,𝑡,𝑦,𝑧   𝐵,𝑙,𝑟,𝑠,𝑚,𝑤,𝑦   𝐿,𝑙,𝑟,𝑠,𝑦   𝑚,𝑀,𝑟,𝑠,𝑧   𝑅,𝑙,𝑟,𝑤   𝑆,𝑚,𝑠,𝑡   𝜑,𝑟,𝑠,𝑙,𝑚,𝑡,𝑤,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑤)   𝐵(𝑧,𝑡)   𝑅(𝑦,𝑧,𝑡,𝑚,𝑠)   𝑆(𝑦,𝑧,𝑤,𝑟,𝑙)   𝐿(𝑧,𝑤,𝑡,𝑚)   𝑀(𝑦,𝑤,𝑡,𝑙)

Proof of Theorem addsunif
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addsunif.3 . . . 4 (𝜑𝐴 = (𝐿 |s 𝑅))
2 addsunif.1 . . . . 5 (𝜑𝐿 <<s 𝑅)
32scutcld 27138 . . . 4 (𝜑 → (𝐿 |s 𝑅) ∈ No )
41, 3eqeltrd 2838 . . 3 (𝜑𝐴 No )
5 addsunif.4 . . . 4 (𝜑𝐵 = (𝑀 |s 𝑆))
6 addsunif.2 . . . . 5 (𝜑𝑀 <<s 𝑆)
76scutcld 27138 . . . 4 (𝜑 → (𝑀 |s 𝑆) ∈ No )
85, 7eqeltrd 2838 . . 3 (𝜑𝐵 No )
9 addsval2 34301 . . 3 ((𝐴 No 𝐵 No ) → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
104, 8, 9syl2anc 584 . 2 (𝜑 → (𝐴 +s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
114, 8addscut 34315 . . . . 5 (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
1211simp2d 1143 . . . 4 (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)})
1311simp3d 1144 . . . 4 (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
14 ovex 7387 . . . . . 6 (𝐴 +s 𝐵) ∈ V
1514snnz 4736 . . . . 5 {(𝐴 +s 𝐵)} ≠ ∅
16 sslttr 27142 . . . . 5 ((({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}) ∧ {(𝐴 +s 𝐵)} ≠ ∅) → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
1715, 16mp3an3 1450 . . . 4 ((({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})) → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
1812, 13, 17syl2anc 584 . . 3 (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
192, 1cofcutr1d 27240 . . . . . 6 (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 𝑝 ≤s 𝑙)
20 leftssno 27206 . . . . . . . . . . 11 ( L ‘𝐴) ⊆ No
2120sseli 3939 . . . . . . . . . 10 (𝑝 ∈ ( L ‘𝐴) → 𝑝 No )
2221ad2antlr 725 . . . . . . . . 9 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → 𝑝 No )
23 ssltss1 27124 . . . . . . . . . . . 12 (𝐿 <<s 𝑅𝐿 No )
242, 23syl 17 . . . . . . . . . . 11 (𝜑𝐿 No )
2524adantr 481 . . . . . . . . . 10 ((𝜑𝑝 ∈ ( L ‘𝐴)) → 𝐿 No )
2625sselda 3943 . . . . . . . . 9 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → 𝑙 No )
278ad2antrr 724 . . . . . . . . 9 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → 𝐵 No )
2822, 26, 27sleadd1d 34330 . . . . . . . 8 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → (𝑝 ≤s 𝑙 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
2928rexbidva 3172 . . . . . . 7 ((𝜑𝑝 ∈ ( L ‘𝐴)) → (∃𝑙𝐿 𝑝 ≤s 𝑙 ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
3029ralbidva 3171 . . . . . 6 (𝜑 → (∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 𝑝 ≤s 𝑙 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
3119, 30mpbid 231 . . . . 5 (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
32 eqeq1 2740 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑠 = (𝑙 +s 𝐵)))
3332rexbidv 3174 . . . . . . . . 9 (𝑦 = 𝑠 → (∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵)))
3433rexab 3651 . . . . . . . 8 (∃𝑠 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑠(∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
35 rexcom4 3270 . . . . . . . . 9 (∃𝑙𝐿𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠𝑙𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
36 ovex 7387 . . . . . . . . . . 11 (𝑙 +s 𝐵) ∈ V
37 breq2 5108 . . . . . . . . . . 11 (𝑠 = (𝑙 +s 𝐵) → ((𝑝 +s 𝐵) ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
3836, 37ceqsexv 3493 . . . . . . . . . 10 (∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
3938rexbii 3096 . . . . . . . . 9 (∃𝑙𝐿𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
40 r19.41v 3184 . . . . . . . . . 10 (∃𝑙𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
4140exbii 1850 . . . . . . . . 9 (∃𝑠𝑙𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠(∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
4235, 39, 413bitr3ri 301 . . . . . . . 8 (∃𝑠(∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
4334, 42bitri 274 . . . . . . 7 (∃𝑠 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
44 ssun1 4131 . . . . . . . 8 {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})
45 ssrexv 4010 . . . . . . . 8 ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) → (∃𝑠 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
4644, 45ax-mp 5 . . . . . . 7 (∃𝑠 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
4743, 46sylbir 234 . . . . . 6 (∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
4847ralimi 3085 . . . . 5 (∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
4931, 48syl 17 . . . 4 (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
506, 5cofcutr1d 27240 . . . . . 6 (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 𝑞 ≤s 𝑚)
51 leftssno 27206 . . . . . . . . . . 11 ( L ‘𝐵) ⊆ No
5251sseli 3939 . . . . . . . . . 10 (𝑞 ∈ ( L ‘𝐵) → 𝑞 No )
5352ad2antlr 725 . . . . . . . . 9 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → 𝑞 No )
54 ssltss1 27124 . . . . . . . . . . . 12 (𝑀 <<s 𝑆𝑀 No )
556, 54syl 17 . . . . . . . . . . 11 (𝜑𝑀 No )
5655adantr 481 . . . . . . . . . 10 ((𝜑𝑞 ∈ ( L ‘𝐵)) → 𝑀 No )
5756sselda 3943 . . . . . . . . 9 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → 𝑚 No )
584ad2antrr 724 . . . . . . . . 9 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → 𝐴 No )
5953, 57, 58sleadd2d 34331 . . . . . . . 8 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → (𝑞 ≤s 𝑚 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6059rexbidva 3172 . . . . . . 7 ((𝜑𝑞 ∈ ( L ‘𝐵)) → (∃𝑚𝑀 𝑞 ≤s 𝑚 ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6160ralbidva 3171 . . . . . 6 (𝜑 → (∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 𝑞 ≤s 𝑚 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6250, 61mpbid 231 . . . . 5 (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
63 eqeq1 2740 . . . . . . . . . 10 (𝑧 = 𝑠 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑠 = (𝐴 +s 𝑚)))
6463rexbidv 3174 . . . . . . . . 9 (𝑧 = 𝑠 → (∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚)))
6564rexab 3651 . . . . . . . 8 (∃𝑠 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑠(∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
66 rexcom4 3270 . . . . . . . . 9 (∃𝑚𝑀𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠𝑚𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
67 ovex 7387 . . . . . . . . . . 11 (𝐴 +s 𝑚) ∈ V
68 breq2 5108 . . . . . . . . . . 11 (𝑠 = (𝐴 +s 𝑚) → ((𝐴 +s 𝑞) ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6967, 68ceqsexv 3493 . . . . . . . . . 10 (∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
7069rexbii 3096 . . . . . . . . 9 (∃𝑚𝑀𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
71 r19.41v 3184 . . . . . . . . . 10 (∃𝑚𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
7271exbii 1850 . . . . . . . . 9 (∃𝑠𝑚𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠(∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
7366, 70, 723bitr3ri 301 . . . . . . . 8 (∃𝑠(∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
7465, 73bitri 274 . . . . . . 7 (∃𝑠 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
75 ssun2 4132 . . . . . . . 8 {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})
76 ssrexv 4010 . . . . . . . 8 ({𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) → (∃𝑠 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
7775, 76ax-mp 5 . . . . . . 7 (∃𝑠 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
7874, 77sylbir 234 . . . . . 6 (∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
7978ralimi 3085 . . . . 5 (∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
8062, 79syl 17 . . . 4 (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
81 ralunb 4150 . . . . 5 (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
82 eqeq1 2740 . . . . . . . . 9 (𝑎 = 𝑟 → (𝑎 = (𝑝 +s 𝐵) ↔ 𝑟 = (𝑝 +s 𝐵)))
8382rexbidv 3174 . . . . . . . 8 (𝑎 = 𝑟 → (∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵)))
8483ralab 3648 . . . . . . 7 (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
85 ralcom4 3268 . . . . . . . 8 (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
86 ovex 7387 . . . . . . . . . 10 (𝑝 +s 𝐵) ∈ V
87 breq1 5107 . . . . . . . . . . 11 (𝑟 = (𝑝 +s 𝐵) → (𝑟 ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s 𝑠))
8887rexbidv 3174 . . . . . . . . . 10 (𝑟 = (𝑝 +s 𝐵) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
8986, 88ceqsalv 3480 . . . . . . . . 9 (∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
9089ralbii 3095 . . . . . . . 8 (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
91 r19.23v 3178 . . . . . . . . 9 (∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
9291albii 1821 . . . . . . . 8 (∀𝑟𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
9385, 90, 923bitr3ri 301 . . . . . . 7 (∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
9484, 93bitri 274 . . . . . 6 (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
95 eqeq1 2740 . . . . . . . . 9 (𝑏 = 𝑟 → (𝑏 = (𝐴 +s 𝑞) ↔ 𝑟 = (𝐴 +s 𝑞)))
9695rexbidv 3174 . . . . . . . 8 (𝑏 = 𝑟 → (∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞)))
9796ralab 3648 . . . . . . 7 (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
98 ralcom4 3268 . . . . . . . 8 (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
99 ovex 7387 . . . . . . . . . 10 (𝐴 +s 𝑞) ∈ V
100 breq1 5107 . . . . . . . . . . 11 (𝑟 = (𝐴 +s 𝑞) → (𝑟 ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s 𝑠))
101100rexbidv 3174 . . . . . . . . . 10 (𝑟 = (𝐴 +s 𝑞) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
10299, 101ceqsalv 3480 . . . . . . . . 9 (∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
103102ralbii 3095 . . . . . . . 8 (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
104 r19.23v 3178 . . . . . . . . 9 (∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
105104albii 1821 . . . . . . . 8 (∀𝑟𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
10698, 103, 1053bitr3ri 301 . . . . . . 7 (∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
10797, 106bitri 274 . . . . . 6 (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
10894, 107anbi12i 627 . . . . 5 ((∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
10981, 108bitri 274 . . . 4 (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
11049, 80, 109sylanbrc 583 . . 3 (𝜑 → ∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠)
1112, 1cofcutr2d 27241 . . . . . 6 (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 𝑟 ≤s 𝑒)
112 ssltss2 27125 . . . . . . . . . . . 12 (𝐿 <<s 𝑅𝑅 No )
1132, 112syl 17 . . . . . . . . . . 11 (𝜑𝑅 No )
114113adantr 481 . . . . . . . . . 10 ((𝜑𝑒 ∈ ( R ‘𝐴)) → 𝑅 No )
115114sselda 3943 . . . . . . . . 9 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → 𝑟 No )
116 rightssno 27207 . . . . . . . . . . 11 ( R ‘𝐴) ⊆ No
117116sseli 3939 . . . . . . . . . 10 (𝑒 ∈ ( R ‘𝐴) → 𝑒 No )
118117ad2antlr 725 . . . . . . . . 9 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → 𝑒 No )
1198ad2antrr 724 . . . . . . . . 9 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → 𝐵 No )
120115, 118, 119sleadd1d 34330 . . . . . . . 8 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → (𝑟 ≤s 𝑒 ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
121120rexbidva 3172 . . . . . . 7 ((𝜑𝑒 ∈ ( R ‘𝐴)) → (∃𝑟𝑅 𝑟 ≤s 𝑒 ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
122121ralbidva 3171 . . . . . 6 (𝜑 → (∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 𝑟 ≤s 𝑒 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
123111, 122mpbid 231 . . . . 5 (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
124 eqeq1 2740 . . . . . . . . . 10 (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝐵) ↔ 𝑏 = (𝑟 +s 𝐵)))
125124rexbidv 3174 . . . . . . . . 9 (𝑤 = 𝑏 → (∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵) ↔ ∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵)))
126125rexab 3651 . . . . . . . 8 (∃𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑏(∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
127 rexcom4 3270 . . . . . . . . 9 (∃𝑟𝑅𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏𝑟𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
128 ovex 7387 . . . . . . . . . . 11 (𝑟 +s 𝐵) ∈ V
129 breq1 5107 . . . . . . . . . . 11 (𝑏 = (𝑟 +s 𝐵) → (𝑏 ≤s (𝑒 +s 𝐵) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
130128, 129ceqsexv 3493 . . . . . . . . . 10 (∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
131130rexbii 3096 . . . . . . . . 9 (∃𝑟𝑅𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
132 r19.41v 3184 . . . . . . . . . 10 (∃𝑟𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
133132exbii 1850 . . . . . . . . 9 (∃𝑏𝑟𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏(∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
134127, 131, 1333bitr3ri 301 . . . . . . . 8 (∃𝑏(∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
135126, 134bitri 274 . . . . . . 7 (∃𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
136 ssun1 4131 . . . . . . . 8 {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})
137 ssrexv 4010 . . . . . . . 8 ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → (∃𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
138136, 137ax-mp 5 . . . . . . 7 (∃𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
139135, 138sylbir 234 . . . . . 6 (∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
140139ralimi 3085 . . . . 5 (∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
141123, 140syl 17 . . . 4 (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
1426, 5cofcutr2d 27241 . . . . . 6 (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 𝑠 ≤s 𝑓)
143 ssltss2 27125 . . . . . . . . . . . 12 (𝑀 <<s 𝑆𝑆 No )
1446, 143syl 17 . . . . . . . . . . 11 (𝜑𝑆 No )
145144adantr 481 . . . . . . . . . 10 ((𝜑𝑓 ∈ ( R ‘𝐵)) → 𝑆 No )
146145sselda 3943 . . . . . . . . 9 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → 𝑠 No )
147 rightssno 27207 . . . . . . . . . . 11 ( R ‘𝐵) ⊆ No
148147sseli 3939 . . . . . . . . . 10 (𝑓 ∈ ( R ‘𝐵) → 𝑓 No )
149148ad2antlr 725 . . . . . . . . 9 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → 𝑓 No )
1504ad2antrr 724 . . . . . . . . 9 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → 𝐴 No )
151146, 149, 150sleadd2d 34331 . . . . . . . 8 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → (𝑠 ≤s 𝑓 ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
152151rexbidva 3172 . . . . . . 7 ((𝜑𝑓 ∈ ( R ‘𝐵)) → (∃𝑠𝑆 𝑠 ≤s 𝑓 ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
153152ralbidva 3171 . . . . . 6 (𝜑 → (∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 𝑠 ≤s 𝑓 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
154142, 153mpbid 231 . . . . 5 (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
155 eqeq1 2740 . . . . . . . . . 10 (𝑡 = 𝑏 → (𝑡 = (𝐴 +s 𝑠) ↔ 𝑏 = (𝐴 +s 𝑠)))
156155rexbidv 3174 . . . . . . . . 9 (𝑡 = 𝑏 → (∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠) ↔ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)))
157156rexab 3651 . . . . . . . 8 (∃𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑏(∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
158 rexcom4 3270 . . . . . . . . 9 (∃𝑠𝑆𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏𝑠𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
159 ovex 7387 . . . . . . . . . . 11 (𝐴 +s 𝑠) ∈ V
160 breq1 5107 . . . . . . . . . . 11 (𝑏 = (𝐴 +s 𝑠) → (𝑏 ≤s (𝐴 +s 𝑓) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
161159, 160ceqsexv 3493 . . . . . . . . . 10 (∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
162161rexbii 3096 . . . . . . . . 9 (∃𝑠𝑆𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
163 r19.41v 3184 . . . . . . . . . 10 (∃𝑠𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
164163exbii 1850 . . . . . . . . 9 (∃𝑏𝑠𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏(∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
165158, 162, 1643bitr3ri 301 . . . . . . . 8 (∃𝑏(∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
166157, 165bitri 274 . . . . . . 7 (∃𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
167 ssun2 4132 . . . . . . . 8 {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})
168 ssrexv 4010 . . . . . . . 8 ({𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → (∃𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
169167, 168ax-mp 5 . . . . . . 7 (∃𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
170166, 169sylbir 234 . . . . . 6 (∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
171170ralimi 3085 . . . . 5 (∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
172154, 171syl 17 . . . 4 (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
173 ralunb 4150 . . . . 5 (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
174 eqeq1 2740 . . . . . . . . 9 (𝑐 = 𝑎 → (𝑐 = (𝑒 +s 𝐵) ↔ 𝑎 = (𝑒 +s 𝐵)))
175174rexbidv 3174 . . . . . . . 8 (𝑐 = 𝑎 → (∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵) ↔ ∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵)))
176175ralab 3648 . . . . . . 7 (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
177 ralcom4 3268 . . . . . . . 8 (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
178 ovex 7387 . . . . . . . . . 10 (𝑒 +s 𝐵) ∈ V
179 breq2 5108 . . . . . . . . . . 11 (𝑎 = (𝑒 +s 𝐵) → (𝑏 ≤s 𝑎𝑏 ≤s (𝑒 +s 𝐵)))
180179rexbidv 3174 . . . . . . . . . 10 (𝑎 = (𝑒 +s 𝐵) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
181178, 180ceqsalv 3480 . . . . . . . . 9 (∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
182181ralbii 3095 . . . . . . . 8 (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
183 r19.23v 3178 . . . . . . . . 9 (∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
184183albii 1821 . . . . . . . 8 (∀𝑎𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
185177, 182, 1843bitr3ri 301 . . . . . . 7 (∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
186176, 185bitri 274 . . . . . 6 (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
187 eqeq1 2740 . . . . . . . . 9 (𝑑 = 𝑎 → (𝑑 = (𝐴 +s 𝑓) ↔ 𝑎 = (𝐴 +s 𝑓)))
188187rexbidv 3174 . . . . . . . 8 (𝑑 = 𝑎 → (∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓) ↔ ∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓)))
189188ralab 3648 . . . . . . 7 (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
190 ralcom4 3268 . . . . . . . 8 (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
191 ovex 7387 . . . . . . . . . 10 (𝐴 +s 𝑓) ∈ V
192 breq2 5108 . . . . . . . . . . 11 (𝑎 = (𝐴 +s 𝑓) → (𝑏 ≤s 𝑎𝑏 ≤s (𝐴 +s 𝑓)))
193192rexbidv 3174 . . . . . . . . . 10 (𝑎 = (𝐴 +s 𝑓) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
194191, 193ceqsalv 3480 . . . . . . . . 9 (∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
195194ralbii 3095 . . . . . . . 8 (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
196 r19.23v 3178 . . . . . . . . 9 (∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
197196albii 1821 . . . . . . . 8 (∀𝑎𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
198190, 195, 1973bitr3ri 301 . . . . . . 7 (∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
199189, 198bitri 274 . . . . . 6 (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
200186, 199anbi12i 627 . . . . 5 ((∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
201173, 200bitri 274 . . . 4 (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
202141, 172, 201sylanbrc 583 . . 3 (𝜑 → ∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎)
203 eqid 2736 . . . . . . . 8 (𝑙𝐿 ↦ (𝑙 +s 𝐵)) = (𝑙𝐿 ↦ (𝑙 +s 𝐵))
204203rnmpt 5909 . . . . . . 7 ran (𝑙𝐿 ↦ (𝑙 +s 𝐵)) = {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)}
205 ssltex1 27122 . . . . . . . . . 10 (𝐿 <<s 𝑅𝐿 ∈ V)
2062, 205syl 17 . . . . . . . . 9 (𝜑𝐿 ∈ V)
207206mptexd 7171 . . . . . . . 8 (𝜑 → (𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
208 rnexg 7838 . . . . . . . 8 ((𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V → ran (𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
209207, 208syl 17 . . . . . . 7 (𝜑 → ran (𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
210204, 209eqeltrrid 2843 . . . . . 6 (𝜑 → {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∈ V)
211 eqid 2736 . . . . . . . 8 (𝑚𝑀 ↦ (𝐴 +s 𝑚)) = (𝑚𝑀 ↦ (𝐴 +s 𝑚))
212211rnmpt 5909 . . . . . . 7 ran (𝑚𝑀 ↦ (𝐴 +s 𝑚)) = {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}
213 ssltex1 27122 . . . . . . . . . 10 (𝑀 <<s 𝑆𝑀 ∈ V)
2146, 213syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ V)
215214mptexd 7171 . . . . . . . 8 (𝜑 → (𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
216 rnexg 7838 . . . . . . . 8 ((𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V → ran (𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
217215, 216syl 17 . . . . . . 7 (𝜑 → ran (𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
218212, 217eqeltrrid 2843 . . . . . 6 (𝜑 → {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ∈ V)
219210, 218unexd 7685 . . . . 5 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ∈ V)
220 snex 5387 . . . . . 6 {(𝐴 +s 𝐵)} ∈ V
221220a1i 11 . . . . 5 (𝜑 → {(𝐴 +s 𝐵)} ∈ V)
22224sselda 3943 . . . . . . . . . 10 ((𝜑𝑙𝐿) → 𝑙 No )
2238adantr 481 . . . . . . . . . 10 ((𝜑𝑙𝐿) → 𝐵 No )
224222, 223addscld 34316 . . . . . . . . 9 ((𝜑𝑙𝐿) → (𝑙 +s 𝐵) ∈ No )
225 eleq1 2825 . . . . . . . . 9 (𝑦 = (𝑙 +s 𝐵) → (𝑦 No ↔ (𝑙 +s 𝐵) ∈ No ))
226224, 225syl5ibrcom 246 . . . . . . . 8 ((𝜑𝑙𝐿) → (𝑦 = (𝑙 +s 𝐵) → 𝑦 No ))
227226rexlimdva 3151 . . . . . . 7 (𝜑 → (∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵) → 𝑦 No ))
228227abssdv 4024 . . . . . 6 (𝜑 → {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ No )
2294adantr 481 . . . . . . . . . 10 ((𝜑𝑚𝑀) → 𝐴 No )
23055sselda 3943 . . . . . . . . . 10 ((𝜑𝑚𝑀) → 𝑚 No )
231229, 230addscld 34316 . . . . . . . . 9 ((𝜑𝑚𝑀) → (𝐴 +s 𝑚) ∈ No )
232 eleq1 2825 . . . . . . . . 9 (𝑧 = (𝐴 +s 𝑚) → (𝑧 No ↔ (𝐴 +s 𝑚) ∈ No ))
233231, 232syl5ibrcom 246 . . . . . . . 8 ((𝜑𝑚𝑀) → (𝑧 = (𝐴 +s 𝑚) → 𝑧 No ))
234233rexlimdva 3151 . . . . . . 7 (𝜑 → (∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚) → 𝑧 No ))
235234abssdv 4024 . . . . . 6 (𝜑 → {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ No )
236228, 235unssd 4145 . . . . 5 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ⊆ No )
2374, 8addscld 34316 . . . . . 6 (𝜑 → (𝐴 +s 𝐵) ∈ No )
238237snssd 4768 . . . . 5 (𝜑 → {(𝐴 +s 𝐵)} ⊆ No )
239 velsn 4601 . . . . . . 7 (𝑏 ∈ {(𝐴 +s 𝐵)} ↔ 𝑏 = (𝐴 +s 𝐵))
240 elun 4107 . . . . . . . . . . 11 (𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (𝑎 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}))
241 vex 3448 . . . . . . . . . . . . 13 𝑎 ∈ V
242 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑦 = 𝑎 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑎 = (𝑙 +s 𝐵)))
243242rexbidv 3174 . . . . . . . . . . . . 13 (𝑦 = 𝑎 → (∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵)))
244241, 243elab 3629 . . . . . . . . . . . 12 (𝑎 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ↔ ∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵))
245 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑧 = 𝑎 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑎 = (𝐴 +s 𝑚)))
246245rexbidv 3174 . . . . . . . . . . . . 13 (𝑧 = 𝑎 → (∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)))
247241, 246elab 3629 . . . . . . . . . . . 12 (𝑎 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ↔ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚))
248244, 247orbi12i 913 . . . . . . . . . . 11 ((𝑎 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)))
249240, 248bitri 274 . . . . . . . . . 10 (𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)))
250 scutcut 27136 . . . . . . . . . . . . . . . . . . 19 (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
2512, 250syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 |s 𝑅) ∈ No 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
252251simp2d 1143 . . . . . . . . . . . . . . . . 17 (𝜑𝐿 <<s {(𝐿 |s 𝑅)})
253252adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑙𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)})
254 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑙𝐿) → 𝑙𝐿)
255 ovex 7387 . . . . . . . . . . . . . . . . . 18 (𝐿 |s 𝑅) ∈ V
256255snid 4621 . . . . . . . . . . . . . . . . 17 (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)}
257256a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑙𝐿) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
258253, 254, 257ssltsepcd 27129 . . . . . . . . . . . . . . 15 ((𝜑𝑙𝐿) → 𝑙 <s (𝐿 |s 𝑅))
2591adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑙𝐿) → 𝐴 = (𝐿 |s 𝑅))
260258, 259breqtrrd 5132 . . . . . . . . . . . . . 14 ((𝜑𝑙𝐿) → 𝑙 <s 𝐴)
2614adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑙𝐿) → 𝐴 No )
262222, 261, 223sltadd1d 34333 . . . . . . . . . . . . . 14 ((𝜑𝑙𝐿) → (𝑙 <s 𝐴 ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
263260, 262mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑙𝐿) → (𝑙 +s 𝐵) <s (𝐴 +s 𝐵))
264 breq1 5107 . . . . . . . . . . . . 13 (𝑎 = (𝑙 +s 𝐵) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
265263, 264syl5ibrcom 246 . . . . . . . . . . . 12 ((𝜑𝑙𝐿) → (𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
266265rexlimdva 3151 . . . . . . . . . . 11 (𝜑 → (∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
267 scutcut 27136 . . . . . . . . . . . . . . . . . . 19 (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
2686, 267syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑀 |s 𝑆) ∈ No 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
269268simp2d 1143 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 <<s {(𝑀 |s 𝑆)})
270269adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑀) → 𝑀 <<s {(𝑀 |s 𝑆)})
271 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑀) → 𝑚𝑀)
272 ovex 7387 . . . . . . . . . . . . . . . . . 18 (𝑀 |s 𝑆) ∈ V
273272snid 4621 . . . . . . . . . . . . . . . . 17 (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
274273a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
275270, 271, 274ssltsepcd 27129 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑀) → 𝑚 <s (𝑀 |s 𝑆))
2765adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑀) → 𝐵 = (𝑀 |s 𝑆))
277275, 276breqtrrd 5132 . . . . . . . . . . . . . 14 ((𝜑𝑚𝑀) → 𝑚 <s 𝐵)
2788adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑀) → 𝐵 No )
279230, 278, 229sltadd2d 34332 . . . . . . . . . . . . . 14 ((𝜑𝑚𝑀) → (𝑚 <s 𝐵 ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
280277, 279mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑚𝑀) → (𝐴 +s 𝑚) <s (𝐴 +s 𝐵))
281 breq1 5107 . . . . . . . . . . . . 13 (𝑎 = (𝐴 +s 𝑚) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
282280, 281syl5ibrcom 246 . . . . . . . . . . . 12 ((𝜑𝑚𝑀) → (𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
283282rexlimdva 3151 . . . . . . . . . . 11 (𝜑 → (∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
284266, 283jaod 857 . . . . . . . . . 10 (𝜑 → ((∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)) → 𝑎 <s (𝐴 +s 𝐵)))
285249, 284biimtrid 241 . . . . . . . . 9 (𝜑 → (𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) → 𝑎 <s (𝐴 +s 𝐵)))
286285imp 407 . . . . . . . 8 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})) → 𝑎 <s (𝐴 +s 𝐵))
287 breq2 5108 . . . . . . . 8 (𝑏 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏𝑎 <s (𝐴 +s 𝐵)))
288286, 287syl5ibrcom 246 . . . . . . 7 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
289239, 288biimtrid 241 . . . . . 6 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 ∈ {(𝐴 +s 𝐵)} → 𝑎 <s 𝑏))
2902893impia 1117 . . . . 5 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ∧ 𝑏 ∈ {(𝐴 +s 𝐵)}) → 𝑎 <s 𝑏)
291219, 221, 236, 238, 290ssltd 27127 . . . 4 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)})
29210sneqd 4597 . . . 4 (𝜑 → {(𝐴 +s 𝐵)} = {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
293291, 292breqtrd 5130 . . 3 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
294 eqid 2736 . . . . . . . 8 (𝑟𝑅 ↦ (𝑟 +s 𝐵)) = (𝑟𝑅 ↦ (𝑟 +s 𝐵))
295294rnmpt 5909 . . . . . . 7 ran (𝑟𝑅 ↦ (𝑟 +s 𝐵)) = {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}
296 ssltex2 27123 . . . . . . . . . 10 (𝐿 <<s 𝑅𝑅 ∈ V)
2972, 296syl 17 . . . . . . . . 9 (𝜑𝑅 ∈ V)
298297mptexd 7171 . . . . . . . 8 (𝜑 → (𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
299 rnexg 7838 . . . . . . . 8 ((𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V → ran (𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
300298, 299syl 17 . . . . . . 7 (𝜑 → ran (𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
301295, 300eqeltrrid 2843 . . . . . 6 (𝜑 → {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∈ V)
302 eqid 2736 . . . . . . . 8 (𝑠𝑆 ↦ (𝐴 +s 𝑠)) = (𝑠𝑆 ↦ (𝐴 +s 𝑠))
303302rnmpt 5909 . . . . . . 7 ran (𝑠𝑆 ↦ (𝐴 +s 𝑠)) = {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}
304 ssltex2 27123 . . . . . . . . . 10 (𝑀 <<s 𝑆𝑆 ∈ V)
3056, 304syl 17 . . . . . . . . 9 (𝜑𝑆 ∈ V)
306305mptexd 7171 . . . . . . . 8 (𝜑 → (𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
307 rnexg 7838 . . . . . . . 8 ((𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V → ran (𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
308306, 307syl 17 . . . . . . 7 (𝜑 → ran (𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
309303, 308eqeltrrid 2843 . . . . . 6 (𝜑 → {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ∈ V)
310301, 309unexd 7685 . . . . 5 (𝜑 → ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ∈ V)
311113sselda 3943 . . . . . . . . . 10 ((𝜑𝑟𝑅) → 𝑟 No )
3128adantr 481 . . . . . . . . . 10 ((𝜑𝑟𝑅) → 𝐵 No )
313311, 312addscld 34316 . . . . . . . . 9 ((𝜑𝑟𝑅) → (𝑟 +s 𝐵) ∈ No )
314 eleq1 2825 . . . . . . . . 9 (𝑤 = (𝑟 +s 𝐵) → (𝑤 No ↔ (𝑟 +s 𝐵) ∈ No ))
315313, 314syl5ibrcom 246 . . . . . . . 8 ((𝜑𝑟𝑅) → (𝑤 = (𝑟 +s 𝐵) → 𝑤 No ))
316315rexlimdva 3151 . . . . . . 7 (𝜑 → (∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵) → 𝑤 No ))
317316abssdv 4024 . . . . . 6 (𝜑 → {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ No )
3184adantr 481 . . . . . . . . . 10 ((𝜑𝑠𝑆) → 𝐴 No )
319144sselda 3943 . . . . . . . . . 10 ((𝜑𝑠𝑆) → 𝑠 No )
320318, 319addscld 34316 . . . . . . . . 9 ((𝜑𝑠𝑆) → (𝐴 +s 𝑠) ∈ No )
321 eleq1 2825 . . . . . . . . 9 (𝑡 = (𝐴 +s 𝑠) → (𝑡 No ↔ (𝐴 +s 𝑠) ∈ No ))
322320, 321syl5ibrcom 246 . . . . . . . 8 ((𝜑𝑠𝑆) → (𝑡 = (𝐴 +s 𝑠) → 𝑡 No ))
323322rexlimdva 3151 . . . . . . 7 (𝜑 → (∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠) → 𝑡 No ))
324323abssdv 4024 . . . . . 6 (𝜑 → {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ No )
325317, 324unssd 4145 . . . . 5 (𝜑 → ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ⊆ No )
326 velsn 4601 . . . . . . 7 (𝑎 ∈ {(𝐴 +s 𝐵)} ↔ 𝑎 = (𝐴 +s 𝐵))
327 elun 4107 . . . . . . . . . . . . 13 (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}))
328 vex 3448 . . . . . . . . . . . . . . 15 𝑏 ∈ V
329328, 125elab 3629 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ↔ ∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵))
330328, 156elab 3629 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ↔ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠))
331329, 330orbi12i 913 . . . . . . . . . . . . 13 ((𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)))
332327, 331bitri 274 . . . . . . . . . . . 12 (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)))
3331adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑅) → 𝐴 = (𝐿 |s 𝑅))
334251simp3d 1144 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅)
335334adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅)
336256a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑅) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
337 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑅) → 𝑟𝑅)
338335, 336, 337ssltsepcd 27129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑅) → (𝐿 |s 𝑅) <s 𝑟)
339333, 338eqbrtrd 5126 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑅) → 𝐴 <s 𝑟)
3404adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑅) → 𝐴 No )
341340, 311, 312sltadd1d 34333 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑅) → (𝐴 <s 𝑟 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
342339, 341mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑟𝑅) → (𝐴 +s 𝐵) <s (𝑟 +s 𝐵))
343 breq2 5108 . . . . . . . . . . . . . . 15 (𝑏 = (𝑟 +s 𝐵) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
344342, 343syl5ibrcom 246 . . . . . . . . . . . . . 14 ((𝜑𝑟𝑅) → (𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
345344rexlimdva 3151 . . . . . . . . . . . . 13 (𝜑 → (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
3465adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝑆) → 𝐵 = (𝑀 |s 𝑆))
347268simp3d 1144 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {(𝑀 |s 𝑆)} <<s 𝑆)
348347adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠𝑆) → {(𝑀 |s 𝑆)} <<s 𝑆)
349273a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠𝑆) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
350 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠𝑆) → 𝑠𝑆)
351348, 349, 350ssltsepcd 27129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝑆) → (𝑀 |s 𝑆) <s 𝑠)
352346, 351eqbrtrd 5126 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝑆) → 𝐵 <s 𝑠)
3538adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝑆) → 𝐵 No )
354353, 319, 318sltadd2d 34332 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝑆) → (𝐵 <s 𝑠 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
355352, 354mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝑆) → (𝐴 +s 𝐵) <s (𝐴 +s 𝑠))
356 breq2 5108 . . . . . . . . . . . . . . 15 (𝑏 = (𝐴 +s 𝑠) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
357355, 356syl5ibrcom 246 . . . . . . . . . . . . . 14 ((𝜑𝑠𝑆) → (𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
358357rexlimdva 3151 . . . . . . . . . . . . 13 (𝜑 → (∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
359345, 358jaod 857 . . . . . . . . . . . 12 (𝜑 → ((∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)) → (𝐴 +s 𝐵) <s 𝑏))
360332, 359biimtrid 241 . . . . . . . . . . 11 (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝐴 +s 𝐵) <s 𝑏))
361360imp 407 . . . . . . . . . 10 ((𝜑𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝐴 +s 𝐵) <s 𝑏)
362 breq1 5107 . . . . . . . . . 10 (𝑎 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ (𝐴 +s 𝐵) <s 𝑏))
363361, 362syl5ibrcom 246 . . . . . . . . 9 ((𝜑𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
364363ex 413 . . . . . . . 8 (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏)))
365364com23 86 . . . . . . 7 (𝜑 → (𝑎 = (𝐴 +s 𝐵) → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
366326, 365biimtrid 241 . . . . . 6 (𝜑 → (𝑎 ∈ {(𝐴 +s 𝐵)} → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
3673663imp 1111 . . . . 5 ((𝜑𝑎 ∈ {(𝐴 +s 𝐵)} ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})) → 𝑎 <s 𝑏)
368221, 310, 238, 325, 367ssltd 27127 . . . 4 (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}))
369292, 368eqbrtrrd 5128 . . 3 (𝜑 → {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))} <<s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}))
37018, 110, 202, 293, 369cofcut1d 27236 . 2 (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})) = (({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})))
37110, 370eqtrd 2776 1 (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wne 2942  wral 3063  wrex 3072  Vcvv 3444  cun 3907  wss 3909  c0 4281  {csn 4585   class class class wbr 5104  cmpt 5187  ran crn 5633  cfv 6494  (class class class)co 7354   No csur 26984   <s cslt 26985   ≤s csle 27088   <<s csslt 27116   |s cscut 27118   L cleft 27171   R cright 27172   +s cadds 34297
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 2707  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-ot 4594  df-uni 4865  df-int 4907  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-se 5588  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7310  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7918  df-2nd 7919  df-frecs 8209  df-wrecs 8240  df-recs 8314  df-1o 8409  df-2o 8410  df-nadd 8609  df-no 26987  df-slt 26988  df-bday 26989  df-sle 27089  df-sslt 27117  df-scut 27119  df-0s 27159  df-made 27173  df-old 27174  df-left 27176  df-right 27177  df-norec2 27257  df-adds 34298
This theorem is referenced by:  addsasslem1  34337  addsasslem2  34338  negsid  34365
  Copyright terms: Public domain W3C validator