MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addsuniflem Structured version   Visualization version   GIF version

Theorem addsuniflem 28034
Description: Lemma for addsunif 28035. State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025.)
Hypotheses
Ref Expression
addsuniflem.1 (𝜑𝐿 <<s 𝑅)
addsuniflem.2 (𝜑𝑀 <<s 𝑆)
addsuniflem.3 (𝜑𝐴 = (𝐿 |s 𝑅))
addsuniflem.4 (𝜑𝐵 = (𝑀 |s 𝑆))
Assertion
Ref Expression
addsuniflem (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})))
Distinct variable groups:   𝐴,𝑙   𝐴,𝑚,𝑟,𝑠   𝑡,𝐴   𝑧,𝐴   𝐵,𝑙   𝐵,𝑚,𝑟,𝑠   𝑤,𝐵   𝑦,𝐵   𝐿,𝑙,𝑟,𝑠,𝑦   𝑚,𝑀,𝑟,𝑠,𝑧   𝑅,𝑙,𝑟   𝑤,𝑅   𝑆,𝑚,𝑠   𝑡,𝑆   𝜑,𝑙,𝑟,𝑠,𝑦   𝜑,𝑚,𝑧   𝜑,𝑡   𝜑,𝑤,𝑟   𝑡,𝑠
Allowed substitution hints:   𝐴(𝑦,𝑤)   𝐵(𝑧,𝑡)   𝑅(𝑦,𝑧,𝑡,𝑚,𝑠)   𝑆(𝑦,𝑧,𝑤,𝑟,𝑙)   𝐿(𝑧,𝑤,𝑡,𝑚)   𝑀(𝑦,𝑤,𝑡,𝑙)

Proof of Theorem addsuniflem
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addsuniflem.3 . . . 4 (𝜑𝐴 = (𝐿 |s 𝑅))
2 addsuniflem.1 . . . . 5 (𝜑𝐿 <<s 𝑅)
32scutcld 27848 . . . 4 (𝜑 → (𝐿 |s 𝑅) ∈ No )
41, 3eqeltrd 2841 . . 3 (𝜑𝐴 No )
5 addsuniflem.4 . . . 4 (𝜑𝐵 = (𝑀 |s 𝑆))
6 addsuniflem.2 . . . . 5 (𝜑𝑀 <<s 𝑆)
76scutcld 27848 . . . 4 (𝜑 → (𝑀 |s 𝑆) ∈ No )
85, 7eqeltrd 2841 . . 3 (𝜑𝐵 No )
9 addsval2 27996 . . 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 28011 . . . . 5 (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})))
1211simp2d 1144 . . . 4 (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) <<s {(𝐴 +s 𝐵)})
1311simp3d 1145 . . . 4 (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))
14 ovex 7464 . . . . . 6 (𝐴 +s 𝐵) ∈ V
1514snnz 4776 . . . . 5 {(𝐴 +s 𝐵)} ≠ ∅
16 sslttr 27852 . . . . 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 1452 . . . 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 27959 . . . . . 6 (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 𝑝 ≤s 𝑙)
20 leftssno 27919 . . . . . . . . . . 11 ( L ‘𝐴) ⊆ No
2120sseli 3979 . . . . . . . . . 10 (𝑝 ∈ ( L ‘𝐴) → 𝑝 No )
2221ad2antlr 727 . . . . . . . . 9 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → 𝑝 No )
23 ssltss1 27833 . . . . . . . . . . . 12 (𝐿 <<s 𝑅𝐿 No )
242, 23syl 17 . . . . . . . . . . 11 (𝜑𝐿 No )
2524adantr 480 . . . . . . . . . 10 ((𝜑𝑝 ∈ ( L ‘𝐴)) → 𝐿 No )
2625sselda 3983 . . . . . . . . 9 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → 𝑙 No )
278ad2antrr 726 . . . . . . . . 9 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → 𝐵 No )
2822, 26, 27sleadd1d 28028 . . . . . . . 8 (((𝜑𝑝 ∈ ( L ‘𝐴)) ∧ 𝑙𝐿) → (𝑝 ≤s 𝑙 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
2928rexbidva 3177 . . . . . . 7 ((𝜑𝑝 ∈ ( L ‘𝐴)) → (∃𝑙𝐿 𝑝 ≤s 𝑙 ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
3029ralbidva 3176 . . . . . 6 (𝜑 → (∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 𝑝 ≤s 𝑙 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
3119, 30mpbid 232 . . . . 5 (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
32 eqeq1 2741 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑠 = (𝑙 +s 𝐵)))
3332rexbidv 3179 . . . . . . . . 9 (𝑦 = 𝑠 → (∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵)))
3433rexab 3700 . . . . . . . 8 (∃𝑠 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑠(∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
35 rexcom4 3288 . . . . . . . . 9 (∃𝑙𝐿𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠𝑙𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
36 ovex 7464 . . . . . . . . . . 11 (𝑙 +s 𝐵) ∈ V
37 breq2 5147 . . . . . . . . . . 11 (𝑠 = (𝑙 +s 𝐵) → ((𝑝 +s 𝐵) ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵)))
3836, 37ceqsexv 3532 . . . . . . . . . 10 (∃𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
3938rexbii 3094 . . . . . . . . 9 (∃𝑙𝐿𝑠(𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
40 r19.41v 3189 . . . . . . . . . 10 (∃𝑙𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ (∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
4140exbii 1848 . . . . . . . . 9 (∃𝑠𝑙𝐿 (𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑠(∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠))
4235, 39, 413bitr3ri 302 . . . . . . . 8 (∃𝑠(∃𝑙𝐿 𝑠 = (𝑙 +s 𝐵) ∧ (𝑝 +s 𝐵) ≤s 𝑠) ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
4334, 42bitri 275 . . . . . . 7 (∃𝑠 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} (𝑝 +s 𝐵) ≤s 𝑠 ↔ ∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵))
44 ssun1 4178 . . . . . . . 8 {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})
45 ssrexv 4053 . . . . . . . 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 235 . . . . . 6 (∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
4847ralimi 3083 . . . . 5 (∀𝑝 ∈ ( L ‘𝐴)∃𝑙𝐿 (𝑝 +s 𝐵) ≤s (𝑙 +s 𝐵) → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
4931, 48syl 17 . . . 4 (𝜑 → ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
506, 5cofcutr1d 27959 . . . . . 6 (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 𝑞 ≤s 𝑚)
51 leftssno 27919 . . . . . . . . . . 11 ( L ‘𝐵) ⊆ No
5251sseli 3979 . . . . . . . . . 10 (𝑞 ∈ ( L ‘𝐵) → 𝑞 No )
5352ad2antlr 727 . . . . . . . . 9 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → 𝑞 No )
54 ssltss1 27833 . . . . . . . . . . . 12 (𝑀 <<s 𝑆𝑀 No )
556, 54syl 17 . . . . . . . . . . 11 (𝜑𝑀 No )
5655adantr 480 . . . . . . . . . 10 ((𝜑𝑞 ∈ ( L ‘𝐵)) → 𝑀 No )
5756sselda 3983 . . . . . . . . 9 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → 𝑚 No )
584ad2antrr 726 . . . . . . . . 9 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → 𝐴 No )
5953, 57, 58sleadd2d 28029 . . . . . . . 8 (((𝜑𝑞 ∈ ( L ‘𝐵)) ∧ 𝑚𝑀) → (𝑞 ≤s 𝑚 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6059rexbidva 3177 . . . . . . 7 ((𝜑𝑞 ∈ ( L ‘𝐵)) → (∃𝑚𝑀 𝑞 ≤s 𝑚 ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6160ralbidva 3176 . . . . . 6 (𝜑 → (∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 𝑞 ≤s 𝑚 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6250, 61mpbid 232 . . . . 5 (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
63 eqeq1 2741 . . . . . . . . . 10 (𝑧 = 𝑠 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑠 = (𝐴 +s 𝑚)))
6463rexbidv 3179 . . . . . . . . 9 (𝑧 = 𝑠 → (∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚)))
6564rexab 3700 . . . . . . . 8 (∃𝑠 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑠(∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
66 rexcom4 3288 . . . . . . . . 9 (∃𝑚𝑀𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠𝑚𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
67 ovex 7464 . . . . . . . . . . 11 (𝐴 +s 𝑚) ∈ V
68 breq2 5147 . . . . . . . . . . 11 (𝑠 = (𝐴 +s 𝑚) → ((𝐴 +s 𝑞) ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚)))
6967, 68ceqsexv 3532 . . . . . . . . . 10 (∃𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
7069rexbii 3094 . . . . . . . . 9 (∃𝑚𝑀𝑠(𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
71 r19.41v 3189 . . . . . . . . . 10 (∃𝑚𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ (∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
7271exbii 1848 . . . . . . . . 9 (∃𝑠𝑚𝑀 (𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑠(∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠))
7366, 70, 723bitr3ri 302 . . . . . . . 8 (∃𝑠(∃𝑚𝑀 𝑠 = (𝐴 +s 𝑚) ∧ (𝐴 +s 𝑞) ≤s 𝑠) ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
7465, 73bitri 275 . . . . . . 7 (∃𝑠 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} (𝐴 +s 𝑞) ≤s 𝑠 ↔ ∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚))
75 ssun2 4179 . . . . . . . 8 {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})
76 ssrexv 4053 . . . . . . . 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 235 . . . . . 6 (∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
7978ralimi 3083 . . . . 5 (∀𝑞 ∈ ( L ‘𝐵)∃𝑚𝑀 (𝐴 +s 𝑞) ≤s (𝐴 +s 𝑚) → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
8062, 79syl 17 . . . 4 (𝜑 → ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
81 ralunb 4197 . . . . 5 (∀𝑟 ∈ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)})∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
82 eqeq1 2741 . . . . . . . . 9 (𝑎 = 𝑟 → (𝑎 = (𝑝 +s 𝐵) ↔ 𝑟 = (𝑝 +s 𝐵)))
8382rexbidv 3179 . . . . . . . 8 (𝑎 = 𝑟 → (∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵)))
8483ralab 3697 . . . . . . 7 (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
85 ralcom4 3286 . . . . . . . 8 (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
86 ovex 7464 . . . . . . . . . 10 (𝑝 +s 𝐵) ∈ V
87 breq1 5146 . . . . . . . . . . 11 (𝑟 = (𝑝 +s 𝐵) → (𝑟 ≤s 𝑠 ↔ (𝑝 +s 𝐵) ≤s 𝑠))
8887rexbidv 3179 . . . . . . . . . 10 (𝑟 = (𝑝 +s 𝐵) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠))
8986, 88ceqsalv 3521 . . . . . . . . 9 (∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
9089ralbii 3093 . . . . . . . 8 (∀𝑝 ∈ ( L ‘𝐴)∀𝑟(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
91 r19.23v 3183 . . . . . . . . 9 (∀𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
9291albii 1819 . . . . . . . 8 (∀𝑟𝑝 ∈ ( L ‘𝐴)(𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
9385, 90, 923bitr3ri 302 . . . . . . 7 (∀𝑟(∃𝑝 ∈ ( L ‘𝐴)𝑟 = (𝑝 +s 𝐵) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
9484, 93bitri 275 . . . . . 6 (∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠)
95 eqeq1 2741 . . . . . . . . 9 (𝑏 = 𝑟 → (𝑏 = (𝐴 +s 𝑞) ↔ 𝑟 = (𝐴 +s 𝑞)))
9695rexbidv 3179 . . . . . . . 8 (𝑏 = 𝑟 → (∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞)))
9796ralab 3697 . . . . . . 7 (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
98 ralcom4 3286 . . . . . . . 8 (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
99 ovex 7464 . . . . . . . . . 10 (𝐴 +s 𝑞) ∈ V
100 breq1 5146 . . . . . . . . . . 11 (𝑟 = (𝐴 +s 𝑞) → (𝑟 ≤s 𝑠 ↔ (𝐴 +s 𝑞) ≤s 𝑠))
101100rexbidv 3179 . . . . . . . . . 10 (𝑟 = (𝐴 +s 𝑞) → (∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
10299, 101ceqsalv 3521 . . . . . . . . 9 (∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
103102ralbii 3093 . . . . . . . 8 (∀𝑞 ∈ ( L ‘𝐵)∀𝑟(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
104 r19.23v 3183 . . . . . . . . 9 (∀𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
105104albii 1819 . . . . . . . 8 (∀𝑟𝑞 ∈ ( L ‘𝐵)(𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠))
10698, 103, 1053bitr3ri 302 . . . . . . 7 (∀𝑟(∃𝑞 ∈ ( L ‘𝐵)𝑟 = (𝐴 +s 𝑞) → ∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
10797, 106bitri 275 . . . . . 6 (∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ↔ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠)
10894, 107anbi12i 628 . . . . 5 ((∀𝑟 ∈ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠 ∧ ∀𝑟 ∈ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})𝑟 ≤s 𝑠) ↔ (∀𝑝 ∈ ( L ‘𝐴)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝑝 +s 𝐵) ≤s 𝑠 ∧ ∀𝑞 ∈ ( L ‘𝐵)∃𝑠 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})(𝐴 +s 𝑞) ≤s 𝑠))
10981, 108bitri 275 . . . 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 27960 . . . . . 6 (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 𝑟 ≤s 𝑒)
112 ssltss2 27834 . . . . . . . . . . . 12 (𝐿 <<s 𝑅𝑅 No )
1132, 112syl 17 . . . . . . . . . . 11 (𝜑𝑅 No )
114113adantr 480 . . . . . . . . . 10 ((𝜑𝑒 ∈ ( R ‘𝐴)) → 𝑅 No )
115114sselda 3983 . . . . . . . . 9 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → 𝑟 No )
116 rightssno 27920 . . . . . . . . . . 11 ( R ‘𝐴) ⊆ No
117116sseli 3979 . . . . . . . . . 10 (𝑒 ∈ ( R ‘𝐴) → 𝑒 No )
118117ad2antlr 727 . . . . . . . . 9 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → 𝑒 No )
1198ad2antrr 726 . . . . . . . . 9 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → 𝐵 No )
120115, 118, 119sleadd1d 28028 . . . . . . . 8 (((𝜑𝑒 ∈ ( R ‘𝐴)) ∧ 𝑟𝑅) → (𝑟 ≤s 𝑒 ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
121120rexbidva 3177 . . . . . . 7 ((𝜑𝑒 ∈ ( R ‘𝐴)) → (∃𝑟𝑅 𝑟 ≤s 𝑒 ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
122121ralbidva 3176 . . . . . 6 (𝜑 → (∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 𝑟 ≤s 𝑒 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
123111, 122mpbid 232 . . . . 5 (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
124 eqeq1 2741 . . . . . . . . . 10 (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝐵) ↔ 𝑏 = (𝑟 +s 𝐵)))
125124rexbidv 3179 . . . . . . . . 9 (𝑤 = 𝑏 → (∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵) ↔ ∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵)))
126125rexab 3700 . . . . . . . 8 (∃𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑏(∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
127 rexcom4 3288 . . . . . . . . 9 (∃𝑟𝑅𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏𝑟𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
128 ovex 7464 . . . . . . . . . . 11 (𝑟 +s 𝐵) ∈ V
129 breq1 5146 . . . . . . . . . . 11 (𝑏 = (𝑟 +s 𝐵) → (𝑏 ≤s (𝑒 +s 𝐵) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵)))
130128, 129ceqsexv 3532 . . . . . . . . . 10 (∃𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
131130rexbii 3094 . . . . . . . . 9 (∃𝑟𝑅𝑏(𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
132 r19.41v 3189 . . . . . . . . . 10 (∃𝑟𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
133132exbii 1848 . . . . . . . . 9 (∃𝑏𝑟𝑅 (𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑏(∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)))
134127, 131, 1333bitr3ri 302 . . . . . . . 8 (∃𝑏(∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∧ 𝑏 ≤s (𝑒 +s 𝐵)) ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
135126, 134bitri 275 . . . . . . 7 (∃𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}𝑏 ≤s (𝑒 +s 𝐵) ↔ ∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵))
136 ssun1 4178 . . . . . . . 8 {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})
137 ssrexv 4053 . . . . . . . 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 235 . . . . . 6 (∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
140139ralimi 3083 . . . . 5 (∀𝑒 ∈ ( R ‘𝐴)∃𝑟𝑅 (𝑟 +s 𝐵) ≤s (𝑒 +s 𝐵) → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
141123, 140syl 17 . . . 4 (𝜑 → ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
1426, 5cofcutr2d 27960 . . . . . 6 (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 𝑠 ≤s 𝑓)
143 ssltss2 27834 . . . . . . . . . . . 12 (𝑀 <<s 𝑆𝑆 No )
1446, 143syl 17 . . . . . . . . . . 11 (𝜑𝑆 No )
145144adantr 480 . . . . . . . . . 10 ((𝜑𝑓 ∈ ( R ‘𝐵)) → 𝑆 No )
146145sselda 3983 . . . . . . . . 9 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → 𝑠 No )
147 rightssno 27920 . . . . . . . . . . 11 ( R ‘𝐵) ⊆ No
148147sseli 3979 . . . . . . . . . 10 (𝑓 ∈ ( R ‘𝐵) → 𝑓 No )
149148ad2antlr 727 . . . . . . . . 9 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → 𝑓 No )
1504ad2antrr 726 . . . . . . . . 9 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → 𝐴 No )
151146, 149, 150sleadd2d 28029 . . . . . . . 8 (((𝜑𝑓 ∈ ( R ‘𝐵)) ∧ 𝑠𝑆) → (𝑠 ≤s 𝑓 ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
152151rexbidva 3177 . . . . . . 7 ((𝜑𝑓 ∈ ( R ‘𝐵)) → (∃𝑠𝑆 𝑠 ≤s 𝑓 ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
153152ralbidva 3176 . . . . . 6 (𝜑 → (∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 𝑠 ≤s 𝑓 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
154142, 153mpbid 232 . . . . 5 (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
155 eqeq1 2741 . . . . . . . . . 10 (𝑡 = 𝑏 → (𝑡 = (𝐴 +s 𝑠) ↔ 𝑏 = (𝐴 +s 𝑠)))
156155rexbidv 3179 . . . . . . . . 9 (𝑡 = 𝑏 → (∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠) ↔ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)))
157156rexab 3700 . . . . . . . 8 (∃𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑏(∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
158 rexcom4 3288 . . . . . . . . 9 (∃𝑠𝑆𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏𝑠𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
159 ovex 7464 . . . . . . . . . . 11 (𝐴 +s 𝑠) ∈ V
160 breq1 5146 . . . . . . . . . . 11 (𝑏 = (𝐴 +s 𝑠) → (𝑏 ≤s (𝐴 +s 𝑓) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓)))
161159, 160ceqsexv 3532 . . . . . . . . . 10 (∃𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
162161rexbii 3094 . . . . . . . . 9 (∃𝑠𝑆𝑏(𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
163 r19.41v 3189 . . . . . . . . . 10 (∃𝑠𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ (∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
164163exbii 1848 . . . . . . . . 9 (∃𝑏𝑠𝑆 (𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑏(∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)))
165158, 162, 1643bitr3ri 302 . . . . . . . 8 (∃𝑏(∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) ∧ 𝑏 ≤s (𝐴 +s 𝑓)) ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
166157, 165bitri 275 . . . . . . 7 (∃𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}𝑏 ≤s (𝐴 +s 𝑓) ↔ ∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓))
167 ssun2 4179 . . . . . . . 8 {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})
168 ssrexv 4053 . . . . . . . 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 235 . . . . . 6 (∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
171170ralimi 3083 . . . . 5 (∀𝑓 ∈ ( R ‘𝐵)∃𝑠𝑆 (𝐴 +s 𝑠) ≤s (𝐴 +s 𝑓) → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
172154, 171syl 17 . . . 4 (𝜑 → ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
173 ralunb 4197 . . . . 5 (∀𝑎 ∈ ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
174 eqeq1 2741 . . . . . . . . 9 (𝑐 = 𝑎 → (𝑐 = (𝑒 +s 𝐵) ↔ 𝑎 = (𝑒 +s 𝐵)))
175174rexbidv 3179 . . . . . . . 8 (𝑐 = 𝑎 → (∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵) ↔ ∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵)))
176175ralab 3697 . . . . . . 7 (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
177 ralcom4 3286 . . . . . . . 8 (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
178 ovex 7464 . . . . . . . . . 10 (𝑒 +s 𝐵) ∈ V
179 breq2 5147 . . . . . . . . . . 11 (𝑎 = (𝑒 +s 𝐵) → (𝑏 ≤s 𝑎𝑏 ≤s (𝑒 +s 𝐵)))
180179rexbidv 3179 . . . . . . . . . 10 (𝑎 = (𝑒 +s 𝐵) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵)))
181178, 180ceqsalv 3521 . . . . . . . . 9 (∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
182181ralbii 3093 . . . . . . . 8 (∀𝑒 ∈ ( R ‘𝐴)∀𝑎(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
183 r19.23v 3183 . . . . . . . . 9 (∀𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
184183albii 1819 . . . . . . . 8 (∀𝑎𝑒 ∈ ( R ‘𝐴)(𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
185177, 182, 1843bitr3ri 302 . . . . . . 7 (∀𝑎(∃𝑒 ∈ ( R ‘𝐴)𝑎 = (𝑒 +s 𝐵) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
186176, 185bitri 275 . . . . . 6 (∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵))
187 eqeq1 2741 . . . . . . . . 9 (𝑑 = 𝑎 → (𝑑 = (𝐴 +s 𝑓) ↔ 𝑎 = (𝐴 +s 𝑓)))
188187rexbidv 3179 . . . . . . . 8 (𝑑 = 𝑎 → (∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓) ↔ ∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓)))
189188ralab 3697 . . . . . . 7 (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
190 ralcom4 3286 . . . . . . . 8 (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
191 ovex 7464 . . . . . . . . . 10 (𝐴 +s 𝑓) ∈ V
192 breq2 5147 . . . . . . . . . . 11 (𝑎 = (𝐴 +s 𝑓) → (𝑏 ≤s 𝑎𝑏 ≤s (𝐴 +s 𝑓)))
193192rexbidv 3179 . . . . . . . . . 10 (𝑎 = (𝐴 +s 𝑓) → (∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
194191, 193ceqsalv 3521 . . . . . . . . 9 (∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
195194ralbii 3093 . . . . . . . 8 (∀𝑓 ∈ ( R ‘𝐵)∀𝑎(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
196 r19.23v 3183 . . . . . . . . 9 (∀𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
197196albii 1819 . . . . . . . 8 (∀𝑎𝑓 ∈ ( R ‘𝐵)(𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎))
198190, 195, 1973bitr3ri 302 . . . . . . 7 (∀𝑎(∃𝑓 ∈ ( R ‘𝐵)𝑎 = (𝐴 +s 𝑓) → ∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
199189, 198bitri 275 . . . . . 6 (∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ↔ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓))
200186, 199anbi12i 628 . . . . 5 ((∀𝑎 ∈ {𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎 ∧ ∀𝑎 ∈ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s 𝑎) ↔ (∀𝑒 ∈ ( R ‘𝐴)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝑒 +s 𝐵) ∧ ∀𝑓 ∈ ( R ‘𝐵)∃𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})𝑏 ≤s (𝐴 +s 𝑓)))
201173, 200bitri 275 . . . 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 2737 . . . . . . . 8 (𝑙𝐿 ↦ (𝑙 +s 𝐵)) = (𝑙𝐿 ↦ (𝑙 +s 𝐵))
204203rnmpt 5968 . . . . . . 7 ran (𝑙𝐿 ↦ (𝑙 +s 𝐵)) = {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)}
205 ssltex1 27831 . . . . . . . . . 10 (𝐿 <<s 𝑅𝐿 ∈ V)
2062, 205syl 17 . . . . . . . . 9 (𝜑𝐿 ∈ V)
207206mptexd 7244 . . . . . . . 8 (𝜑 → (𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
208 rnexg 7924 . . . . . . . 8 ((𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V → ran (𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
209207, 208syl 17 . . . . . . 7 (𝜑 → ran (𝑙𝐿 ↦ (𝑙 +s 𝐵)) ∈ V)
210204, 209eqeltrrid 2846 . . . . . 6 (𝜑 → {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∈ V)
211 eqid 2737 . . . . . . . 8 (𝑚𝑀 ↦ (𝐴 +s 𝑚)) = (𝑚𝑀 ↦ (𝐴 +s 𝑚))
212211rnmpt 5968 . . . . . . 7 ran (𝑚𝑀 ↦ (𝐴 +s 𝑚)) = {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}
213 ssltex1 27831 . . . . . . . . . 10 (𝑀 <<s 𝑆𝑀 ∈ V)
2146, 213syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ V)
215214mptexd 7244 . . . . . . . 8 (𝜑 → (𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
216 rnexg 7924 . . . . . . . 8 ((𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V → ran (𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
217215, 216syl 17 . . . . . . 7 (𝜑 → ran (𝑚𝑀 ↦ (𝐴 +s 𝑚)) ∈ V)
218212, 217eqeltrrid 2846 . . . . . 6 (𝜑 → {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ∈ V)
219210, 218unexd 7774 . . . . 5 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ∈ V)
220 snex 5436 . . . . . 6 {(𝐴 +s 𝐵)} ∈ V
221220a1i 11 . . . . 5 (𝜑 → {(𝐴 +s 𝐵)} ∈ V)
22224sselda 3983 . . . . . . . . . 10 ((𝜑𝑙𝐿) → 𝑙 No )
2238adantr 480 . . . . . . . . . 10 ((𝜑𝑙𝐿) → 𝐵 No )
224222, 223addscld 28013 . . . . . . . . 9 ((𝜑𝑙𝐿) → (𝑙 +s 𝐵) ∈ No )
225 eleq1 2829 . . . . . . . . 9 (𝑦 = (𝑙 +s 𝐵) → (𝑦 No ↔ (𝑙 +s 𝐵) ∈ No ))
226224, 225syl5ibrcom 247 . . . . . . . 8 ((𝜑𝑙𝐿) → (𝑦 = (𝑙 +s 𝐵) → 𝑦 No ))
227226rexlimdva 3155 . . . . . . 7 (𝜑 → (∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵) → 𝑦 No ))
228227abssdv 4068 . . . . . 6 (𝜑 → {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ⊆ No )
2294adantr 480 . . . . . . . . . 10 ((𝜑𝑚𝑀) → 𝐴 No )
23055sselda 3983 . . . . . . . . . 10 ((𝜑𝑚𝑀) → 𝑚 No )
231229, 230addscld 28013 . . . . . . . . 9 ((𝜑𝑚𝑀) → (𝐴 +s 𝑚) ∈ No )
232 eleq1 2829 . . . . . . . . 9 (𝑧 = (𝐴 +s 𝑚) → (𝑧 No ↔ (𝐴 +s 𝑚) ∈ No ))
233231, 232syl5ibrcom 247 . . . . . . . 8 ((𝜑𝑚𝑀) → (𝑧 = (𝐴 +s 𝑚) → 𝑧 No ))
234233rexlimdva 3155 . . . . . . 7 (𝜑 → (∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚) → 𝑧 No ))
235234abssdv 4068 . . . . . 6 (𝜑 → {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ⊆ No )
236228, 235unssd 4192 . . . . 5 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ⊆ No )
2374, 8addscld 28013 . . . . . 6 (𝜑 → (𝐴 +s 𝐵) ∈ No )
238237snssd 4809 . . . . 5 (𝜑 → {(𝐴 +s 𝐵)} ⊆ No )
239 velsn 4642 . . . . . . 7 (𝑏 ∈ {(𝐴 +s 𝐵)} ↔ 𝑏 = (𝐴 +s 𝐵))
240 elun 4153 . . . . . . . . . . 11 (𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (𝑎 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}))
241 vex 3484 . . . . . . . . . . . . 13 𝑎 ∈ V
242 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑦 = 𝑎 → (𝑦 = (𝑙 +s 𝐵) ↔ 𝑎 = (𝑙 +s 𝐵)))
243242rexbidv 3179 . . . . . . . . . . . . 13 (𝑦 = 𝑎 → (∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵) ↔ ∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵)))
244241, 243elab 3679 . . . . . . . . . . . 12 (𝑎 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ↔ ∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵))
245 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑧 = 𝑎 → (𝑧 = (𝐴 +s 𝑚) ↔ 𝑎 = (𝐴 +s 𝑚)))
246245rexbidv 3179 . . . . . . . . . . . . 13 (𝑧 = 𝑎 → (∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚) ↔ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)))
247241, 246elab 3679 . . . . . . . . . . . 12 (𝑎 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)} ↔ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚))
248244, 247orbi12i 915 . . . . . . . . . . 11 ((𝑎 ∈ {𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∨ 𝑎 ∈ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)))
249240, 248bitri 275 . . . . . . . . . 10 (𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ↔ (∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)))
250 scutcut 27846 . . . . . . . . . . . . . . . . . . 19 (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
2512, 250syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 |s 𝑅) ∈ No 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
252251simp2d 1144 . . . . . . . . . . . . . . . . 17 (𝜑𝐿 <<s {(𝐿 |s 𝑅)})
253252adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑙𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)})
254 simpr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑙𝐿) → 𝑙𝐿)
255 ovex 7464 . . . . . . . . . . . . . . . . . 18 (𝐿 |s 𝑅) ∈ V
256255snid 4662 . . . . . . . . . . . . . . . . 17 (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)}
257256a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑙𝐿) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
258253, 254, 257ssltsepcd 27839 . . . . . . . . . . . . . . 15 ((𝜑𝑙𝐿) → 𝑙 <s (𝐿 |s 𝑅))
2591adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑙𝐿) → 𝐴 = (𝐿 |s 𝑅))
260258, 259breqtrrd 5171 . . . . . . . . . . . . . 14 ((𝜑𝑙𝐿) → 𝑙 <s 𝐴)
2614adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑙𝐿) → 𝐴 No )
262222, 261, 223sltadd1d 28031 . . . . . . . . . . . . . 14 ((𝜑𝑙𝐿) → (𝑙 <s 𝐴 ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
263260, 262mpbid 232 . . . . . . . . . . . . 13 ((𝜑𝑙𝐿) → (𝑙 +s 𝐵) <s (𝐴 +s 𝐵))
264 breq1 5146 . . . . . . . . . . . . 13 (𝑎 = (𝑙 +s 𝐵) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝑙 +s 𝐵) <s (𝐴 +s 𝐵)))
265263, 264syl5ibrcom 247 . . . . . . . . . . . 12 ((𝜑𝑙𝐿) → (𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
266265rexlimdva 3155 . . . . . . . . . . 11 (𝜑 → (∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) → 𝑎 <s (𝐴 +s 𝐵)))
267 scutcut 27846 . . . . . . . . . . . . . . . . . . 19 (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
2686, 267syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑀 |s 𝑆) ∈ No 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
269268simp2d 1144 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 <<s {(𝑀 |s 𝑆)})
270269adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑀) → 𝑀 <<s {(𝑀 |s 𝑆)})
271 simpr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑀) → 𝑚𝑀)
272 ovex 7464 . . . . . . . . . . . . . . . . . 18 (𝑀 |s 𝑆) ∈ V
273272snid 4662 . . . . . . . . . . . . . . . . 17 (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
274273a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
275270, 271, 274ssltsepcd 27839 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑀) → 𝑚 <s (𝑀 |s 𝑆))
2765adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑀) → 𝐵 = (𝑀 |s 𝑆))
277275, 276breqtrrd 5171 . . . . . . . . . . . . . 14 ((𝜑𝑚𝑀) → 𝑚 <s 𝐵)
2788adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑀) → 𝐵 No )
279230, 278, 229sltadd2d 28030 . . . . . . . . . . . . . 14 ((𝜑𝑚𝑀) → (𝑚 <s 𝐵 ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
280277, 279mpbid 232 . . . . . . . . . . . . 13 ((𝜑𝑚𝑀) → (𝐴 +s 𝑚) <s (𝐴 +s 𝐵))
281 breq1 5146 . . . . . . . . . . . . 13 (𝑎 = (𝐴 +s 𝑚) → (𝑎 <s (𝐴 +s 𝐵) ↔ (𝐴 +s 𝑚) <s (𝐴 +s 𝐵)))
282280, 281syl5ibrcom 247 . . . . . . . . . . . 12 ((𝜑𝑚𝑀) → (𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
283282rexlimdva 3155 . . . . . . . . . . 11 (𝜑 → (∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚) → 𝑎 <s (𝐴 +s 𝐵)))
284266, 283jaod 860 . . . . . . . . . 10 (𝜑 → ((∃𝑙𝐿 𝑎 = (𝑙 +s 𝐵) ∨ ∃𝑚𝑀 𝑎 = (𝐴 +s 𝑚)) → 𝑎 <s (𝐴 +s 𝐵)))
285249, 284biimtrid 242 . . . . . . . . 9 (𝜑 → (𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) → 𝑎 <s (𝐴 +s 𝐵)))
286285imp 406 . . . . . . . 8 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})) → 𝑎 <s (𝐴 +s 𝐵))
287 breq2 5147 . . . . . . . 8 (𝑏 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏𝑎 <s (𝐴 +s 𝐵)))
288286, 287syl5ibrcom 247 . . . . . . 7 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
289239, 288biimtrid 242 . . . . . 6 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)})) → (𝑏 ∈ {(𝐴 +s 𝐵)} → 𝑎 <s 𝑏))
2902893impia 1118 . . . . 5 ((𝜑𝑎 ∈ ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) ∧ 𝑏 ∈ {(𝐴 +s 𝐵)}) → 𝑎 <s 𝑏)
291219, 221, 236, 238, 290ssltd 27836 . . . 4 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)})
29210sneqd 4638 . . . 4 (𝜑 → {(𝐴 +s 𝐵)} = {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
293291, 292breqtrd 5169 . . 3 (𝜑 → ({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) <<s {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))})
294 eqid 2737 . . . . . . . 8 (𝑟𝑅 ↦ (𝑟 +s 𝐵)) = (𝑟𝑅 ↦ (𝑟 +s 𝐵))
295294rnmpt 5968 . . . . . . 7 ran (𝑟𝑅 ↦ (𝑟 +s 𝐵)) = {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)}
296 ssltex2 27832 . . . . . . . . . 10 (𝐿 <<s 𝑅𝑅 ∈ V)
2972, 296syl 17 . . . . . . . . 9 (𝜑𝑅 ∈ V)
298297mptexd 7244 . . . . . . . 8 (𝜑 → (𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
299 rnexg 7924 . . . . . . . 8 ((𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V → ran (𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
300298, 299syl 17 . . . . . . 7 (𝜑 → ran (𝑟𝑅 ↦ (𝑟 +s 𝐵)) ∈ V)
301295, 300eqeltrrid 2846 . . . . . 6 (𝜑 → {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∈ V)
302 eqid 2737 . . . . . . . 8 (𝑠𝑆 ↦ (𝐴 +s 𝑠)) = (𝑠𝑆 ↦ (𝐴 +s 𝑠))
303302rnmpt 5968 . . . . . . 7 ran (𝑠𝑆 ↦ (𝐴 +s 𝑠)) = {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}
304 ssltex2 27832 . . . . . . . . . 10 (𝑀 <<s 𝑆𝑆 ∈ V)
3056, 304syl 17 . . . . . . . . 9 (𝜑𝑆 ∈ V)
306305mptexd 7244 . . . . . . . 8 (𝜑 → (𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
307 rnexg 7924 . . . . . . . 8 ((𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V → ran (𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
308306, 307syl 17 . . . . . . 7 (𝜑 → ran (𝑠𝑆 ↦ (𝐴 +s 𝑠)) ∈ V)
309303, 308eqeltrrid 2846 . . . . . 6 (𝜑 → {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ∈ V)
310301, 309unexd 7774 . . . . 5 (𝜑 → ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ∈ V)
311113sselda 3983 . . . . . . . . . 10 ((𝜑𝑟𝑅) → 𝑟 No )
3128adantr 480 . . . . . . . . . 10 ((𝜑𝑟𝑅) → 𝐵 No )
313311, 312addscld 28013 . . . . . . . . 9 ((𝜑𝑟𝑅) → (𝑟 +s 𝐵) ∈ No )
314 eleq1 2829 . . . . . . . . 9 (𝑤 = (𝑟 +s 𝐵) → (𝑤 No ↔ (𝑟 +s 𝐵) ∈ No ))
315313, 314syl5ibrcom 247 . . . . . . . 8 ((𝜑𝑟𝑅) → (𝑤 = (𝑟 +s 𝐵) → 𝑤 No ))
316315rexlimdva 3155 . . . . . . 7 (𝜑 → (∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵) → 𝑤 No ))
317316abssdv 4068 . . . . . 6 (𝜑 → {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ⊆ No )
3184adantr 480 . . . . . . . . . 10 ((𝜑𝑠𝑆) → 𝐴 No )
319144sselda 3983 . . . . . . . . . 10 ((𝜑𝑠𝑆) → 𝑠 No )
320318, 319addscld 28013 . . . . . . . . 9 ((𝜑𝑠𝑆) → (𝐴 +s 𝑠) ∈ No )
321 eleq1 2829 . . . . . . . . 9 (𝑡 = (𝐴 +s 𝑠) → (𝑡 No ↔ (𝐴 +s 𝑠) ∈ No ))
322320, 321syl5ibrcom 247 . . . . . . . 8 ((𝜑𝑠𝑆) → (𝑡 = (𝐴 +s 𝑠) → 𝑡 No ))
323322rexlimdva 3155 . . . . . . 7 (𝜑 → (∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠) → 𝑡 No ))
324323abssdv 4068 . . . . . 6 (𝜑 → {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ⊆ No )
325317, 324unssd 4192 . . . . 5 (𝜑 → ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ⊆ No )
326 velsn 4642 . . . . . . 7 (𝑎 ∈ {(𝐴 +s 𝐵)} ↔ 𝑎 = (𝐴 +s 𝐵))
327 elun 4153 . . . . . . . . . . . . 13 (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}))
328 vex 3484 . . . . . . . . . . . . . . 15 𝑏 ∈ V
329328, 125elab 3679 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ↔ ∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵))
330328, 156elab 3679 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)} ↔ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠))
331329, 330orbi12i 915 . . . . . . . . . . . . 13 ((𝑏 ∈ {𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)))
332327, 331bitri 275 . . . . . . . . . . . 12 (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) ↔ (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)))
3331adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑅) → 𝐴 = (𝐿 |s 𝑅))
334251simp3d 1145 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅)
335334adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅)
336256a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑅) → (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)})
337 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑅) → 𝑟𝑅)
338335, 336, 337ssltsepcd 27839 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑅) → (𝐿 |s 𝑅) <s 𝑟)
339333, 338eqbrtrd 5165 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑅) → 𝐴 <s 𝑟)
3404adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑅) → 𝐴 No )
341340, 311, 312sltadd1d 28031 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑅) → (𝐴 <s 𝑟 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
342339, 341mpbid 232 . . . . . . . . . . . . . . 15 ((𝜑𝑟𝑅) → (𝐴 +s 𝐵) <s (𝑟 +s 𝐵))
343 breq2 5147 . . . . . . . . . . . . . . 15 (𝑏 = (𝑟 +s 𝐵) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝑟 +s 𝐵)))
344342, 343syl5ibrcom 247 . . . . . . . . . . . . . 14 ((𝜑𝑟𝑅) → (𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
345344rexlimdva 3155 . . . . . . . . . . . . 13 (𝜑 → (∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) → (𝐴 +s 𝐵) <s 𝑏))
3465adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝑆) → 𝐵 = (𝑀 |s 𝑆))
347268simp3d 1145 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {(𝑀 |s 𝑆)} <<s 𝑆)
348347adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠𝑆) → {(𝑀 |s 𝑆)} <<s 𝑆)
349273a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠𝑆) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
350 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠𝑆) → 𝑠𝑆)
351348, 349, 350ssltsepcd 27839 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝑆) → (𝑀 |s 𝑆) <s 𝑠)
352346, 351eqbrtrd 5165 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝑆) → 𝐵 <s 𝑠)
3538adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝑆) → 𝐵 No )
354353, 319, 318sltadd2d 28030 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝑆) → (𝐵 <s 𝑠 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
355352, 354mpbid 232 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝑆) → (𝐴 +s 𝐵) <s (𝐴 +s 𝑠))
356 breq2 5147 . . . . . . . . . . . . . . 15 (𝑏 = (𝐴 +s 𝑠) → ((𝐴 +s 𝐵) <s 𝑏 ↔ (𝐴 +s 𝐵) <s (𝐴 +s 𝑠)))
357355, 356syl5ibrcom 247 . . . . . . . . . . . . . 14 ((𝜑𝑠𝑆) → (𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
358357rexlimdva 3155 . . . . . . . . . . . . 13 (𝜑 → (∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠) → (𝐴 +s 𝐵) <s 𝑏))
359345, 358jaod 860 . . . . . . . . . . . 12 (𝜑 → ((∃𝑟𝑅 𝑏 = (𝑟 +s 𝐵) ∨ ∃𝑠𝑆 𝑏 = (𝐴 +s 𝑠)) → (𝐴 +s 𝐵) <s 𝑏))
360332, 359biimtrid 242 . . . . . . . . . . 11 (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝐴 +s 𝐵) <s 𝑏))
361360imp 406 . . . . . . . . . 10 ((𝜑𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝐴 +s 𝐵) <s 𝑏)
362 breq1 5146 . . . . . . . . . 10 (𝑎 = (𝐴 +s 𝐵) → (𝑎 <s 𝑏 ↔ (𝐴 +s 𝐵) <s 𝑏))
363361, 362syl5ibrcom 247 . . . . . . . . 9 ((𝜑𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏))
364363ex 412 . . . . . . . 8 (𝜑 → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → (𝑎 = (𝐴 +s 𝐵) → 𝑎 <s 𝑏)))
365364com23 86 . . . . . . 7 (𝜑 → (𝑎 = (𝐴 +s 𝐵) → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
366326, 365biimtrid 242 . . . . . 6 (𝜑 → (𝑎 ∈ {(𝐴 +s 𝐵)} → (𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}) → 𝑎 <s 𝑏)))
3673663imp 1111 . . . . 5 ((𝜑𝑎 ∈ {(𝐴 +s 𝐵)} ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})) → 𝑎 <s 𝑏)
368221, 310, 238, 325, 367ssltd 27836 . . . 4 (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}))
369292, 368eqbrtrrd 5167 . . 3 (𝜑 → {(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)}))} <<s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)}))
37018, 110, 202, 293, 369cofcut1d 27955 . 2 (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)𝑎 = (𝑝 +s 𝐵)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( L ‘𝐵)𝑏 = (𝐴 +s 𝑞)}) |s ({𝑐 ∣ ∃𝑒 ∈ ( R ‘𝐴)𝑐 = (𝑒 +s 𝐵)} ∪ {𝑑 ∣ ∃𝑓 ∈ ( R ‘𝐵)𝑑 = (𝐴 +s 𝑓)})) = (({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})))
37110, 370eqtrd 2777 1 (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠𝑆 𝑡 = (𝐴 +s 𝑠)})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 848  w3a 1087  wal 1538   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wne 2940  wral 3061  wrex 3070  Vcvv 3480  cun 3949  wss 3951  c0 4333  {csn 4626   class class class wbr 5143  cmpt 5225  ran crn 5686  cfv 6561  (class class class)co 7431   No csur 27684   <s cslt 27685   ≤s csle 27789   <<s csslt 27825   |s cscut 27827   L cleft 27884   R cright 27885   +s cadds 27992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-1o 8506  df-2o 8507  df-nadd 8704  df-no 27687  df-slt 27688  df-bday 27689  df-sle 27790  df-sslt 27826  df-scut 27828  df-0s 27869  df-made 27886  df-old 27887  df-left 27889  df-right 27890  df-norec2 27982  df-adds 27993
This theorem is referenced by:  addsunif  28035
  Copyright terms: Public domain W3C validator