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

Theorem addsunif 27313
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 27145 . . . 4 (𝜑 → (ðŋ |s 𝑅) ∈ No )
41, 3eqeltrd 2838 . . 3 (𝜑 → ðī ∈ No )
5 addsunif.4 . . . 4 (𝜑 → ðĩ = (𝑀 |s 𝑆))
6 addsunif.2 . . . . 5 (𝜑 → 𝑀 <<s 𝑆)
76scutcld 27145 . . . 4 (𝜑 → (𝑀 |s 𝑆) ∈ No )
85, 7eqeltrd 2838 . . 3 (𝜑 → ðĩ ∈ No )
9 addsval2 27278 . . 3 ((ðī ∈ No ∧ ðĩ ∈ No ) → (ðī +s ðĩ) = (({𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)} ∊ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)}) |s ({𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)} ∊ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)})))
104, 8, 9syl2anc 585 . 2 (𝜑 → (ðī +s ðĩ) = (({𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)} ∊ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)}) |s ({𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)} ∊ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)})))
114, 8addscut 27292 . . . . 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 7391 . . . . . 6 (ðī +s ðĩ) ∈ V
1514snnz 4738 . . . . 5 {(ðī +s ðĩ)} ≠ ∅
16 sslttr 27149 . . . . 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 1451 . . . 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 585 . . 3 (𝜑 → ({𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)} ∊ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)}) <<s ({𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)} ∊ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)}))
192, 1cofcutr1d 27247 . . . . . 6 (𝜑 → ∀𝑝 ∈ ( L ‘ðī)∃𝑙 ∈ ðŋ 𝑝 â‰Īs 𝑙)
20 leftssno 27213 . . . . . . . . . . 11 ( L ‘ðī) ⊆ No
2120sseli 3941 . . . . . . . . . 10 (𝑝 ∈ ( L ‘ðī) → 𝑝 ∈ No )
2221ad2antlr 726 . . . . . . . . 9 (((𝜑 ∧ 𝑝 ∈ ( L ‘ðī)) ∧ 𝑙 ∈ ðŋ) → 𝑝 ∈ No )
23 ssltss1 27131 . . . . . . . . . . . 12 (ðŋ <<s 𝑅 → ðŋ ⊆ No )
242, 23syl 17 . . . . . . . . . . 11 (𝜑 → ðŋ ⊆ No )
2524adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑝 ∈ ( L ‘ðī)) → ðŋ ⊆ No )
2625sselda 3945 . . . . . . . . 9 (((𝜑 ∧ 𝑝 ∈ ( L ‘ðī)) ∧ 𝑙 ∈ ðŋ) → 𝑙 ∈ No )
278ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ 𝑝 ∈ ( L ‘ðī)) ∧ 𝑙 ∈ ðŋ) → ðĩ ∈ No )
2822, 26, 27sleadd1d 27307 . . . . . . . 8 (((𝜑 ∧ 𝑝 ∈ ( L ‘ðī)) ∧ 𝑙 ∈ ðŋ) → (𝑝 â‰Īs 𝑙 ↔ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ)))
2928rexbidva 3174 . . . . . . 7 ((𝜑 ∧ 𝑝 ∈ ( L ‘ðī)) → (∃𝑙 ∈ ðŋ 𝑝 â‰Īs 𝑙 ↔ ∃𝑙 ∈ ðŋ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ)))
3029ralbidva 3173 . . . . . 6 (𝜑 → (∀𝑝 ∈ ( L ‘ðī)∃𝑙 ∈ ðŋ 𝑝 â‰Īs 𝑙 ↔ ∀𝑝 ∈ ( L ‘ðī)∃𝑙 ∈ ðŋ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ)))
3119, 30mpbid 231 . . . . 5 (𝜑 → ∀𝑝 ∈ ( L ‘ðī)∃𝑙 ∈ ðŋ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ))
32 eqeq1 2741 . . . . . . . . . 10 (ð‘Ķ = 𝑠 → (ð‘Ķ = (𝑙 +s ðĩ) ↔ 𝑠 = (𝑙 +s ðĩ)))
3332rexbidv 3176 . . . . . . . . 9 (ð‘Ķ = 𝑠 → (∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ) ↔ ∃𝑙 ∈ ðŋ 𝑠 = (𝑙 +s ðĩ)))
3433rexab 3653 . . . . . . . 8 (∃𝑠 ∈ {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} (𝑝 +s ðĩ) â‰Īs 𝑠 ↔ ∃𝑠(∃𝑙 ∈ ðŋ 𝑠 = (𝑙 +s ðĩ) ∧ (𝑝 +s ðĩ) â‰Īs 𝑠))
35 rexcom4 3272 . . . . . . . . 9 (∃𝑙 ∈ ðŋ ∃𝑠(𝑠 = (𝑙 +s ðĩ) ∧ (𝑝 +s ðĩ) â‰Īs 𝑠) ↔ ∃𝑠∃𝑙 ∈ ðŋ (𝑠 = (𝑙 +s ðĩ) ∧ (𝑝 +s ðĩ) â‰Īs 𝑠))
36 ovex 7391 . . . . . . . . . . 11 (𝑙 +s ðĩ) ∈ V
37 breq2 5110 . . . . . . . . . . 11 (𝑠 = (𝑙 +s ðĩ) → ((𝑝 +s ðĩ) â‰Īs 𝑠 ↔ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ)))
3836, 37ceqsexv 3495 . . . . . . . . . 10 (∃𝑠(𝑠 = (𝑙 +s ðĩ) ∧ (𝑝 +s ðĩ) â‰Īs 𝑠) ↔ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ))
3938rexbii 3098 . . . . . . . . 9 (∃𝑙 ∈ ðŋ ∃𝑠(𝑠 = (𝑙 +s ðĩ) ∧ (𝑝 +s ðĩ) â‰Īs 𝑠) ↔ ∃𝑙 ∈ ðŋ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ))
40 r19.41v 3186 . . . . . . . . . 10 (∃𝑙 ∈ ðŋ (𝑠 = (𝑙 +s ðĩ) ∧ (𝑝 +s ðĩ) â‰Īs 𝑠) ↔ (∃𝑙 ∈ ðŋ 𝑠 = (𝑙 +s ðĩ) ∧ (𝑝 +s ðĩ) â‰Īs 𝑠))
4140exbii 1851 . . . . . . . . 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 4133 . . . . . . . 8 {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ⊆ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})
45 ssrexv 4012 . . . . . . . 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 3087 . . . . 5 (∀𝑝 ∈ ( L ‘ðī)∃𝑙 ∈ ðŋ (𝑝 +s ðĩ) â‰Īs (𝑙 +s ðĩ) → ∀𝑝 ∈ ( L ‘ðī)∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(𝑝 +s ðĩ) â‰Īs 𝑠)
4931, 48syl 17 . . . 4 (𝜑 → ∀𝑝 ∈ ( L ‘ðī)∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(𝑝 +s ðĩ) â‰Īs 𝑠)
506, 5cofcutr1d 27247 . . . . . 6 (𝜑 → ∀𝑞 ∈ ( L ‘ðĩ)∃𝑚 ∈ 𝑀 𝑞 â‰Īs 𝑚)
51 leftssno 27213 . . . . . . . . . . 11 ( L ‘ðĩ) ⊆ No
5251sseli 3941 . . . . . . . . . 10 (𝑞 ∈ ( L ‘ðĩ) → 𝑞 ∈ No )
5352ad2antlr 726 . . . . . . . . 9 (((𝜑 ∧ 𝑞 ∈ ( L ‘ðĩ)) ∧ 𝑚 ∈ 𝑀) → 𝑞 ∈ No )
54 ssltss1 27131 . . . . . . . . . . . 12 (𝑀 <<s 𝑆 → 𝑀 ⊆ No )
556, 54syl 17 . . . . . . . . . . 11 (𝜑 → 𝑀 ⊆ No )
5655adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑞 ∈ ( L ‘ðĩ)) → 𝑀 ⊆ No )
5756sselda 3945 . . . . . . . . 9 (((𝜑 ∧ 𝑞 ∈ ( L ‘ðĩ)) ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
584ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ 𝑞 ∈ ( L ‘ðĩ)) ∧ 𝑚 ∈ 𝑀) → ðī ∈ No )
5953, 57, 58sleadd2d 27308 . . . . . . . 8 (((𝜑 ∧ 𝑞 ∈ ( L ‘ðĩ)) ∧ 𝑚 ∈ 𝑀) → (𝑞 â‰Īs 𝑚 ↔ (ðī +s 𝑞) â‰Īs (ðī +s 𝑚)))
6059rexbidva 3174 . . . . . . 7 ((𝜑 ∧ 𝑞 ∈ ( L ‘ðĩ)) → (∃𝑚 ∈ 𝑀 𝑞 â‰Īs 𝑚 ↔ ∃𝑚 ∈ 𝑀 (ðī +s 𝑞) â‰Īs (ðī +s 𝑚)))
6160ralbidva 3173 . . . . . 6 (𝜑 → (∀𝑞 ∈ ( L ‘ðĩ)∃𝑚 ∈ 𝑀 𝑞 â‰Īs 𝑚 ↔ ∀𝑞 ∈ ( L ‘ðĩ)∃𝑚 ∈ 𝑀 (ðī +s 𝑞) â‰Īs (ðī +s 𝑚)))
6250, 61mpbid 231 . . . . 5 (𝜑 → ∀𝑞 ∈ ( L ‘ðĩ)∃𝑚 ∈ 𝑀 (ðī +s 𝑞) â‰Īs (ðī +s 𝑚))
63 eqeq1 2741 . . . . . . . . . 10 (𝑧 = 𝑠 → (𝑧 = (ðī +s 𝑚) ↔ 𝑠 = (ðī +s 𝑚)))
6463rexbidv 3176 . . . . . . . . 9 (𝑧 = 𝑠 → (∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑠 = (ðī +s 𝑚)))
6564rexab 3653 . . . . . . . 8 (∃𝑠 ∈ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)} (ðī +s 𝑞) â‰Īs 𝑠 ↔ ∃𝑠(∃𝑚 ∈ 𝑀 𝑠 = (ðī +s 𝑚) ∧ (ðī +s 𝑞) â‰Īs 𝑠))
66 rexcom4 3272 . . . . . . . . 9 (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (ðī +s 𝑚) ∧ (ðī +s 𝑞) â‰Īs 𝑠) ↔ ∃𝑠∃𝑚 ∈ 𝑀 (𝑠 = (ðī +s 𝑚) ∧ (ðī +s 𝑞) â‰Īs 𝑠))
67 ovex 7391 . . . . . . . . . . 11 (ðī +s 𝑚) ∈ V
68 breq2 5110 . . . . . . . . . . 11 (𝑠 = (ðī +s 𝑚) → ((ðī +s 𝑞) â‰Īs 𝑠 ↔ (ðī +s 𝑞) â‰Īs (ðī +s 𝑚)))
6967, 68ceqsexv 3495 . . . . . . . . . 10 (∃𝑠(𝑠 = (ðī +s 𝑚) ∧ (ðī +s 𝑞) â‰Īs 𝑠) ↔ (ðī +s 𝑞) â‰Īs (ðī +s 𝑚))
7069rexbii 3098 . . . . . . . . 9 (∃𝑚 ∈ 𝑀 ∃𝑠(𝑠 = (ðī +s 𝑚) ∧ (ðī +s 𝑞) â‰Īs 𝑠) ↔ ∃𝑚 ∈ 𝑀 (ðī +s 𝑞) â‰Īs (ðī +s 𝑚))
71 r19.41v 3186 . . . . . . . . . 10 (∃𝑚 ∈ 𝑀 (𝑠 = (ðī +s 𝑚) ∧ (ðī +s 𝑞) â‰Īs 𝑠) ↔ (∃𝑚 ∈ 𝑀 𝑠 = (ðī +s 𝑚) ∧ (ðī +s 𝑞) â‰Īs 𝑠))
7271exbii 1851 . . . . . . . . 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 4134 . . . . . . . 8 {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)} ⊆ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})
76 ssrexv 4012 . . . . . . . 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 3087 . . . . 5 (∀𝑞 ∈ ( L ‘ðĩ)∃𝑚 ∈ 𝑀 (ðī +s 𝑞) â‰Īs (ðī +s 𝑚) → ∀𝑞 ∈ ( L ‘ðĩ)∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(ðī +s 𝑞) â‰Īs 𝑠)
8062, 79syl 17 . . . 4 (𝜑 → ∀𝑞 ∈ ( L ‘ðĩ)∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(ðī +s 𝑞) â‰Īs 𝑠)
81 ralunb 4152 . . . . 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 3176 . . . . . . . 8 (𝑎 = 𝑟 → (∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ) ↔ ∃𝑝 ∈ ( L ‘ðī)𝑟 = (𝑝 +s ðĩ)))
8483ralab 3650 . . . . . . 7 (∀𝑟 ∈ {𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)}∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠 ↔ ∀𝑟(∃𝑝 ∈ ( L ‘ðī)𝑟 = (𝑝 +s ðĩ) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠))
85 ralcom4 3270 . . . . . . . 8 (∀𝑝 ∈ ( L ‘ðī)∀𝑟(𝑟 = (𝑝 +s ðĩ) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ ∀𝑟∀𝑝 ∈ ( L ‘ðī)(𝑟 = (𝑝 +s ðĩ) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠))
86 ovex 7391 . . . . . . . . . 10 (𝑝 +s ðĩ) ∈ V
87 breq1 5109 . . . . . . . . . . 11 (𝑟 = (𝑝 +s ðĩ) → (𝑟 â‰Īs 𝑠 ↔ (𝑝 +s ðĩ) â‰Īs 𝑠))
8887rexbidv 3176 . . . . . . . . . 10 (𝑟 = (𝑝 +s ðĩ) → (∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠 ↔ ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(𝑝 +s ðĩ) â‰Īs 𝑠))
8986, 88ceqsalv 3482 . . . . . . . . 9 (∀𝑟(𝑟 = (𝑝 +s ðĩ) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(𝑝 +s ðĩ) â‰Īs 𝑠)
9089ralbii 3097 . . . . . . . 8 (∀𝑝 ∈ ( L ‘ðī)∀𝑟(𝑟 = (𝑝 +s ðĩ) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ ∀𝑝 ∈ ( L ‘ðī)∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(𝑝 +s ðĩ) â‰Īs 𝑠)
91 r19.23v 3180 . . . . . . . . 9 (∀𝑝 ∈ ( L ‘ðī)(𝑟 = (𝑝 +s ðĩ) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ (∃𝑝 ∈ ( L ‘ðī)𝑟 = (𝑝 +s ðĩ) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠))
9291albii 1822 . . . . . . . 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 3176 . . . . . . . 8 (𝑏 = 𝑟 → (∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞) ↔ ∃𝑞 ∈ ( L ‘ðĩ)𝑟 = (ðī +s 𝑞)))
9796ralab 3650 . . . . . . 7 (∀𝑟 ∈ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)}∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠 ↔ ∀𝑟(∃𝑞 ∈ ( L ‘ðĩ)𝑟 = (ðī +s 𝑞) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠))
98 ralcom4 3270 . . . . . . . 8 (∀𝑞 ∈ ( L ‘ðĩ)∀𝑟(𝑟 = (ðī +s 𝑞) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ ∀𝑟∀𝑞 ∈ ( L ‘ðĩ)(𝑟 = (ðī +s 𝑞) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠))
99 ovex 7391 . . . . . . . . . 10 (ðī +s 𝑞) ∈ V
100 breq1 5109 . . . . . . . . . . 11 (𝑟 = (ðī +s 𝑞) → (𝑟 â‰Īs 𝑠 ↔ (ðī +s 𝑞) â‰Īs 𝑠))
101100rexbidv 3176 . . . . . . . . . 10 (𝑟 = (ðī +s 𝑞) → (∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠 ↔ ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(ðī +s 𝑞) â‰Īs 𝑠))
10299, 101ceqsalv 3482 . . . . . . . . 9 (∀𝑟(𝑟 = (ðī +s 𝑞) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(ðī +s 𝑞) â‰Īs 𝑠)
103102ralbii 3097 . . . . . . . 8 (∀𝑞 ∈ ( L ‘ðĩ)∀𝑟(𝑟 = (ðī +s 𝑞) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ ∀𝑞 ∈ ( L ‘ðĩ)∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})(ðī +s 𝑞) â‰Īs 𝑠)
104 r19.23v 3180 . . . . . . . . 9 (∀𝑞 ∈ ( L ‘ðĩ)(𝑟 = (ðī +s 𝑞) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠) ↔ (∃𝑞 ∈ ( L ‘ðĩ)𝑟 = (ðī +s 𝑞) → ∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠))
105104albii 1822 . . . . . . . 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 584 . . 3 (𝜑 → ∀𝑟 ∈ ({𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)} ∊ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)})∃𝑠 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})𝑟 â‰Īs 𝑠)
1112, 1cofcutr2d 27248 . . . . . 6 (𝜑 → ∀𝑒 ∈ ( R ‘ðī)∃𝑟 ∈ 𝑅 𝑟 â‰Īs 𝑒)
112 ssltss2 27132 . . . . . . . . . . . 12 (ðŋ <<s 𝑅 → 𝑅 ⊆ No )
1132, 112syl 17 . . . . . . . . . . 11 (𝜑 → 𝑅 ⊆ No )
114113adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑒 ∈ ( R ‘ðī)) → 𝑅 ⊆ No )
115114sselda 3945 . . . . . . . . 9 (((𝜑 ∧ 𝑒 ∈ ( R ‘ðī)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
116 rightssno 27214 . . . . . . . . . . 11 ( R ‘ðī) ⊆ No
117116sseli 3941 . . . . . . . . . 10 (𝑒 ∈ ( R ‘ðī) → 𝑒 ∈ No )
118117ad2antlr 726 . . . . . . . . 9 (((𝜑 ∧ 𝑒 ∈ ( R ‘ðī)) ∧ 𝑟 ∈ 𝑅) → 𝑒 ∈ No )
1198ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ 𝑒 ∈ ( R ‘ðī)) ∧ 𝑟 ∈ 𝑅) → ðĩ ∈ No )
120115, 118, 119sleadd1d 27307 . . . . . . . 8 (((𝜑 ∧ 𝑒 ∈ ( R ‘ðī)) ∧ 𝑟 ∈ 𝑅) → (𝑟 â‰Īs 𝑒 ↔ (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ)))
121120rexbidva 3174 . . . . . . 7 ((𝜑 ∧ 𝑒 ∈ ( R ‘ðī)) → (∃𝑟 ∈ 𝑅 𝑟 â‰Īs 𝑒 ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ)))
122121ralbidva 3173 . . . . . 6 (𝜑 → (∀𝑒 ∈ ( R ‘ðī)∃𝑟 ∈ 𝑅 𝑟 â‰Īs 𝑒 ↔ ∀𝑒 ∈ ( R ‘ðī)∃𝑟 ∈ 𝑅 (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ)))
123111, 122mpbid 231 . . . . 5 (𝜑 → ∀𝑒 ∈ ( R ‘ðī)∃𝑟 ∈ 𝑅 (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ))
124 eqeq1 2741 . . . . . . . . . 10 (ð‘Ī = 𝑏 → (ð‘Ī = (𝑟 +s ðĩ) ↔ 𝑏 = (𝑟 +s ðĩ)))
125124rexbidv 3176 . . . . . . . . 9 (ð‘Ī = 𝑏 → (∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ) ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ)))
126125rexab 3653 . . . . . . . 8 (∃𝑏 ∈ {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)}𝑏 â‰Īs (𝑒 +s ðĩ) ↔ ∃𝑏(∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ) ∧ 𝑏 â‰Īs (𝑒 +s ðĩ)))
127 rexcom4 3272 . . . . . . . . 9 (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s ðĩ) ∧ 𝑏 â‰Īs (𝑒 +s ðĩ)) ↔ ∃𝑏∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s ðĩ) ∧ 𝑏 â‰Īs (𝑒 +s ðĩ)))
128 ovex 7391 . . . . . . . . . . 11 (𝑟 +s ðĩ) ∈ V
129 breq1 5109 . . . . . . . . . . 11 (𝑏 = (𝑟 +s ðĩ) → (𝑏 â‰Īs (𝑒 +s ðĩ) ↔ (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ)))
130128, 129ceqsexv 3495 . . . . . . . . . 10 (∃𝑏(𝑏 = (𝑟 +s ðĩ) ∧ 𝑏 â‰Īs (𝑒 +s ðĩ)) ↔ (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ))
131130rexbii 3098 . . . . . . . . 9 (∃𝑟 ∈ 𝑅 ∃𝑏(𝑏 = (𝑟 +s ðĩ) ∧ 𝑏 â‰Īs (𝑒 +s ðĩ)) ↔ ∃𝑟 ∈ 𝑅 (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ))
132 r19.41v 3186 . . . . . . . . . 10 (∃𝑟 ∈ 𝑅 (𝑏 = (𝑟 +s ðĩ) ∧ 𝑏 â‰Īs (𝑒 +s ðĩ)) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ) ∧ 𝑏 â‰Īs (𝑒 +s ðĩ)))
133132exbii 1851 . . . . . . . . 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 4133 . . . . . . . 8 {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ⊆ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})
137 ssrexv 4012 . . . . . . . 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 3087 . . . . 5 (∀𝑒 ∈ ( R ‘ðī)∃𝑟 ∈ 𝑅 (𝑟 +s ðĩ) â‰Īs (𝑒 +s ðĩ) → ∀𝑒 ∈ ( R ‘ðī)∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (𝑒 +s ðĩ))
141123, 140syl 17 . . . 4 (𝜑 → ∀𝑒 ∈ ( R ‘ðī)∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (𝑒 +s ðĩ))
1426, 5cofcutr2d 27248 . . . . . 6 (𝜑 → ∀𝑓 ∈ ( R ‘ðĩ)∃𝑠 ∈ 𝑆 𝑠 â‰Īs 𝑓)
143 ssltss2 27132 . . . . . . . . . . . 12 (𝑀 <<s 𝑆 → 𝑆 ⊆ No )
1446, 143syl 17 . . . . . . . . . . 11 (𝜑 → 𝑆 ⊆ No )
145144adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑓 ∈ ( R ‘ðĩ)) → 𝑆 ⊆ No )
146145sselda 3945 . . . . . . . . 9 (((𝜑 ∧ 𝑓 ∈ ( R ‘ðĩ)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
147 rightssno 27214 . . . . . . . . . . 11 ( R ‘ðĩ) ⊆ No
148147sseli 3941 . . . . . . . . . 10 (𝑓 ∈ ( R ‘ðĩ) → 𝑓 ∈ No )
149148ad2antlr 726 . . . . . . . . 9 (((𝜑 ∧ 𝑓 ∈ ( R ‘ðĩ)) ∧ 𝑠 ∈ 𝑆) → 𝑓 ∈ No )
1504ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ 𝑓 ∈ ( R ‘ðĩ)) ∧ 𝑠 ∈ 𝑆) → ðī ∈ No )
151146, 149, 150sleadd2d 27308 . . . . . . . 8 (((𝜑 ∧ 𝑓 ∈ ( R ‘ðĩ)) ∧ 𝑠 ∈ 𝑆) → (𝑠 â‰Īs 𝑓 ↔ (ðī +s 𝑠) â‰Īs (ðī +s 𝑓)))
152151rexbidva 3174 . . . . . . 7 ((𝜑 ∧ 𝑓 ∈ ( R ‘ðĩ)) → (∃𝑠 ∈ 𝑆 𝑠 â‰Īs 𝑓 ↔ ∃𝑠 ∈ 𝑆 (ðī +s 𝑠) â‰Īs (ðī +s 𝑓)))
153152ralbidva 3173 . . . . . 6 (𝜑 → (∀𝑓 ∈ ( R ‘ðĩ)∃𝑠 ∈ 𝑆 𝑠 â‰Īs 𝑓 ↔ ∀𝑓 ∈ ( R ‘ðĩ)∃𝑠 ∈ 𝑆 (ðī +s 𝑠) â‰Īs (ðī +s 𝑓)))
154142, 153mpbid 231 . . . . 5 (𝜑 → ∀𝑓 ∈ ( R ‘ðĩ)∃𝑠 ∈ 𝑆 (ðī +s 𝑠) â‰Īs (ðī +s 𝑓))
155 eqeq1 2741 . . . . . . . . . 10 (ð‘Ą = 𝑏 → (ð‘Ą = (ðī +s 𝑠) ↔ 𝑏 = (ðī +s 𝑠)))
156155rexbidv 3176 . . . . . . . . 9 (ð‘Ą = 𝑏 → (∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠) ↔ ∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠)))
157156rexab 3653 . . . . . . . 8 (∃𝑏 ∈ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}𝑏 â‰Īs (ðī +s 𝑓) ↔ ∃𝑏(∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠) ∧ 𝑏 â‰Īs (ðī +s 𝑓)))
158 rexcom4 3272 . . . . . . . . 9 (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (ðī +s 𝑠) ∧ 𝑏 â‰Īs (ðī +s 𝑓)) ↔ ∃𝑏∃𝑠 ∈ 𝑆 (𝑏 = (ðī +s 𝑠) ∧ 𝑏 â‰Īs (ðī +s 𝑓)))
159 ovex 7391 . . . . . . . . . . 11 (ðī +s 𝑠) ∈ V
160 breq1 5109 . . . . . . . . . . 11 (𝑏 = (ðī +s 𝑠) → (𝑏 â‰Īs (ðī +s 𝑓) ↔ (ðī +s 𝑠) â‰Īs (ðī +s 𝑓)))
161159, 160ceqsexv 3495 . . . . . . . . . 10 (∃𝑏(𝑏 = (ðī +s 𝑠) ∧ 𝑏 â‰Īs (ðī +s 𝑓)) ↔ (ðī +s 𝑠) â‰Īs (ðī +s 𝑓))
162161rexbii 3098 . . . . . . . . 9 (∃𝑠 ∈ 𝑆 ∃𝑏(𝑏 = (ðī +s 𝑠) ∧ 𝑏 â‰Īs (ðī +s 𝑓)) ↔ ∃𝑠 ∈ 𝑆 (ðī +s 𝑠) â‰Īs (ðī +s 𝑓))
163 r19.41v 3186 . . . . . . . . . 10 (∃𝑠 ∈ 𝑆 (𝑏 = (ðī +s 𝑠) ∧ 𝑏 â‰Īs (ðī +s 𝑓)) ↔ (∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠) ∧ 𝑏 â‰Īs (ðī +s 𝑓)))
164163exbii 1851 . . . . . . . . 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 4134 . . . . . . . 8 {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)} ⊆ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})
168 ssrexv 4012 . . . . . . . 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 3087 . . . . 5 (∀𝑓 ∈ ( R ‘ðĩ)∃𝑠 ∈ 𝑆 (ðī +s 𝑠) â‰Īs (ðī +s 𝑓) → ∀𝑓 ∈ ( R ‘ðĩ)∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (ðī +s 𝑓))
172154, 171syl 17 . . . 4 (𝜑 → ∀𝑓 ∈ ( R ‘ðĩ)∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (ðī +s 𝑓))
173 ralunb 4152 . . . . 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 3176 . . . . . . . 8 (𝑐 = 𝑎 → (∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ) ↔ ∃𝑒 ∈ ( R ‘ðī)𝑎 = (𝑒 +s ðĩ)))
176175ralab 3650 . . . . . . 7 (∀𝑎 ∈ {𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)}∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎 ↔ ∀𝑎(∃𝑒 ∈ ( R ‘ðī)𝑎 = (𝑒 +s ðĩ) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎))
177 ralcom4 3270 . . . . . . . 8 (∀𝑒 ∈ ( R ‘ðī)∀𝑎(𝑎 = (𝑒 +s ðĩ) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ ∀𝑎∀𝑒 ∈ ( R ‘ðī)(𝑎 = (𝑒 +s ðĩ) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎))
178 ovex 7391 . . . . . . . . . 10 (𝑒 +s ðĩ) ∈ V
179 breq2 5110 . . . . . . . . . . 11 (𝑎 = (𝑒 +s ðĩ) → (𝑏 â‰Īs 𝑎 ↔ 𝑏 â‰Īs (𝑒 +s ðĩ)))
180179rexbidv 3176 . . . . . . . . . 10 (𝑎 = (𝑒 +s ðĩ) → (∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎 ↔ ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (𝑒 +s ðĩ)))
181178, 180ceqsalv 3482 . . . . . . . . 9 (∀𝑎(𝑎 = (𝑒 +s ðĩ) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (𝑒 +s ðĩ))
182181ralbii 3097 . . . . . . . 8 (∀𝑒 ∈ ( R ‘ðī)∀𝑎(𝑎 = (𝑒 +s ðĩ) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ ∀𝑒 ∈ ( R ‘ðī)∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (𝑒 +s ðĩ))
183 r19.23v 3180 . . . . . . . . 9 (∀𝑒 ∈ ( R ‘ðī)(𝑎 = (𝑒 +s ðĩ) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ (∃𝑒 ∈ ( R ‘ðī)𝑎 = (𝑒 +s ðĩ) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎))
184183albii 1822 . . . . . . . 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 3176 . . . . . . . 8 (𝑑 = 𝑎 → (∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓) ↔ ∃𝑓 ∈ ( R ‘ðĩ)𝑎 = (ðī +s 𝑓)))
189188ralab 3650 . . . . . . 7 (∀𝑎 ∈ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)}∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎 ↔ ∀𝑎(∃𝑓 ∈ ( R ‘ðĩ)𝑎 = (ðī +s 𝑓) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎))
190 ralcom4 3270 . . . . . . . 8 (∀𝑓 ∈ ( R ‘ðĩ)∀𝑎(𝑎 = (ðī +s 𝑓) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ ∀𝑎∀𝑓 ∈ ( R ‘ðĩ)(𝑎 = (ðī +s 𝑓) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎))
191 ovex 7391 . . . . . . . . . 10 (ðī +s 𝑓) ∈ V
192 breq2 5110 . . . . . . . . . . 11 (𝑎 = (ðī +s 𝑓) → (𝑏 â‰Īs 𝑎 ↔ 𝑏 â‰Īs (ðī +s 𝑓)))
193192rexbidv 3176 . . . . . . . . . 10 (𝑎 = (ðī +s 𝑓) → (∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎 ↔ ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (ðī +s 𝑓)))
194191, 193ceqsalv 3482 . . . . . . . . 9 (∀𝑎(𝑎 = (ðī +s 𝑓) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (ðī +s 𝑓))
195194ralbii 3097 . . . . . . . 8 (∀𝑓 ∈ ( R ‘ðĩ)∀𝑎(𝑎 = (ðī +s 𝑓) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ ∀𝑓 ∈ ( R ‘ðĩ)∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs (ðī +s 𝑓))
196 r19.23v 3180 . . . . . . . . 9 (∀𝑓 ∈ ( R ‘ðĩ)(𝑎 = (ðī +s 𝑓) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎) ↔ (∃𝑓 ∈ ( R ‘ðĩ)𝑎 = (ðī +s 𝑓) → ∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎))
197196albii 1822 . . . . . . . 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 584 . . 3 (𝜑 → ∀𝑎 ∈ ({𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)} ∊ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)})∃𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})𝑏 â‰Īs 𝑎)
203 eqid 2737 . . . . . . . 8 (𝑙 ∈ ðŋ â†Ķ (𝑙 +s ðĩ)) = (𝑙 ∈ ðŋ â†Ķ (𝑙 +s ðĩ))
204203rnmpt 5911 . . . . . . 7 ran (𝑙 ∈ ðŋ â†Ķ (𝑙 +s ðĩ)) = {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)}
205 ssltex1 27129 . . . . . . . . . 10 (ðŋ <<s 𝑅 → ðŋ ∈ V)
2062, 205syl 17 . . . . . . . . 9 (𝜑 → ðŋ ∈ V)
207206mptexd 7175 . . . . . . . 8 (𝜑 → (𝑙 ∈ ðŋ â†Ķ (𝑙 +s ðĩ)) ∈ V)
208 rnexg 7842 . . . . . . . 8 ((𝑙 ∈ ðŋ â†Ķ (𝑙 +s ðĩ)) ∈ V → ran (𝑙 ∈ ðŋ â†Ķ (𝑙 +s ðĩ)) ∈ V)
209207, 208syl 17 . . . . . . 7 (𝜑 → ran (𝑙 ∈ ðŋ â†Ķ (𝑙 +s ðĩ)) ∈ V)
210204, 209eqeltrrid 2843 . . . . . 6 (𝜑 → {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∈ V)
211 eqid 2737 . . . . . . . 8 (𝑚 ∈ 𝑀 â†Ķ (ðī +s 𝑚)) = (𝑚 ∈ 𝑀 â†Ķ (ðī +s 𝑚))
212211rnmpt 5911 . . . . . . 7 ran (𝑚 ∈ 𝑀 â†Ķ (ðī +s 𝑚)) = {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}
213 ssltex1 27129 . . . . . . . . . 10 (𝑀 <<s 𝑆 → 𝑀 ∈ V)
2146, 213syl 17 . . . . . . . . 9 (𝜑 → 𝑀 ∈ V)
215214mptexd 7175 . . . . . . . 8 (𝜑 → (𝑚 ∈ 𝑀 â†Ķ (ðī +s 𝑚)) ∈ V)
216 rnexg 7842 . . . . . . . 8 ((𝑚 ∈ 𝑀 â†Ķ (ðī +s 𝑚)) ∈ V → ran (𝑚 ∈ 𝑀 â†Ķ (ðī +s 𝑚)) ∈ V)
217215, 216syl 17 . . . . . . 7 (𝜑 → ran (𝑚 ∈ 𝑀 â†Ķ (ðī +s 𝑚)) ∈ V)
218212, 217eqeltrrid 2843 . . . . . 6 (𝜑 → {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)} ∈ V)
219210, 218unexd 7689 . . . . 5 (𝜑 → ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) ∈ V)
220 snex 5389 . . . . . 6 {(ðī +s ðĩ)} ∈ V
221220a1i 11 . . . . 5 (𝜑 → {(ðī +s ðĩ)} ∈ V)
22224sselda 3945 . . . . . . . . . 10 ((𝜑 ∧ 𝑙 ∈ ðŋ) → 𝑙 ∈ No )
2238adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑙 ∈ ðŋ) → ðĩ ∈ No )
224222, 223addscld 27293 . . . . . . . . 9 ((𝜑 ∧ 𝑙 ∈ ðŋ) → (𝑙 +s ðĩ) ∈ No )
225 eleq1 2826 . . . . . . . . 9 (ð‘Ķ = (𝑙 +s ðĩ) → (ð‘Ķ ∈ No ↔ (𝑙 +s ðĩ) ∈ No ))
226224, 225syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ 𝑙 ∈ ðŋ) → (ð‘Ķ = (𝑙 +s ðĩ) → ð‘Ķ ∈ No ))
227226rexlimdva 3153 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ) → ð‘Ķ ∈ No ))
228227abssdv 4026 . . . . . 6 (𝜑 → {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ⊆ No )
2294adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑚 ∈ 𝑀) → ðī ∈ No )
23055sselda 3945 . . . . . . . . . 10 ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ No )
231229, 230addscld 27293 . . . . . . . . 9 ((𝜑 ∧ 𝑚 ∈ 𝑀) → (ðī +s 𝑚) ∈ No )
232 eleq1 2826 . . . . . . . . 9 (𝑧 = (ðī +s 𝑚) → (𝑧 ∈ No ↔ (ðī +s 𝑚) ∈ No ))
233231, 232syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑧 = (ðī +s 𝑚) → 𝑧 ∈ No ))
234233rexlimdva 3153 . . . . . . 7 (𝜑 → (∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚) → 𝑧 ∈ No ))
235234abssdv 4026 . . . . . 6 (𝜑 → {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)} ⊆ No )
236228, 235unssd 4147 . . . . 5 (𝜑 → ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) ⊆ No )
2374, 8addscld 27293 . . . . . 6 (𝜑 → (ðī +s ðĩ) ∈ No )
238237snssd 4770 . . . . 5 (𝜑 → {(ðī +s ðĩ)} ⊆ No )
239 velsn 4603 . . . . . . 7 (𝑏 ∈ {(ðī +s ðĩ)} ↔ 𝑏 = (ðī +s ðĩ))
240 elun 4109 . . . . . . . . . . 11 (𝑎 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) ↔ (𝑎 ∈ {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} âˆĻ 𝑎 ∈ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}))
241 vex 3450 . . . . . . . . . . . . 13 𝑎 ∈ V
242 eqeq1 2741 . . . . . . . . . . . . . 14 (ð‘Ķ = 𝑎 → (ð‘Ķ = (𝑙 +s ðĩ) ↔ 𝑎 = (𝑙 +s ðĩ)))
243242rexbidv 3176 . . . . . . . . . . . . 13 (ð‘Ķ = 𝑎 → (∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ) ↔ ∃𝑙 ∈ ðŋ 𝑎 = (𝑙 +s ðĩ)))
244241, 243elab 3631 . . . . . . . . . . . 12 (𝑎 ∈ {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ↔ ∃𝑙 ∈ ðŋ 𝑎 = (𝑙 +s ðĩ))
245 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑧 = 𝑎 → (𝑧 = (ðī +s 𝑚) ↔ 𝑎 = (ðī +s 𝑚)))
246245rexbidv 3176 . . . . . . . . . . . . 13 (𝑧 = 𝑎 → (∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚) ↔ ∃𝑚 ∈ 𝑀 𝑎 = (ðī +s 𝑚)))
247241, 246elab 3631 . . . . . . . . . . . 12 (𝑎 ∈ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)} ↔ ∃𝑚 ∈ 𝑀 𝑎 = (ðī +s 𝑚))
248244, 247orbi12i 914 . . . . . . . . . . 11 ((𝑎 ∈ {ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} âˆĻ 𝑎 ∈ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) ↔ (∃𝑙 ∈ ðŋ 𝑎 = (𝑙 +s ðĩ) âˆĻ ∃𝑚 ∈ 𝑀 𝑎 = (ðī +s 𝑚)))
249240, 248bitri 275 . . . . . . . . . 10 (𝑎 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) ↔ (∃𝑙 ∈ ðŋ 𝑎 = (𝑙 +s ðĩ) âˆĻ ∃𝑚 ∈ 𝑀 𝑎 = (ðī +s 𝑚)))
250 scutcut 27143 . . . . . . . . . . . . . . . . . . 19 (ðŋ <<s 𝑅 → ((ðŋ |s 𝑅) ∈ No ∧ ðŋ <<s {(ðŋ |s 𝑅)} ∧ {(ðŋ |s 𝑅)} <<s 𝑅))
2512, 250syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((ðŋ |s 𝑅) ∈ No ∧ ðŋ <<s {(ðŋ |s 𝑅)} ∧ {(ðŋ |s 𝑅)} <<s 𝑅))
252251simp2d 1144 . . . . . . . . . . . . . . . . 17 (𝜑 → ðŋ <<s {(ðŋ |s 𝑅)})
253252adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑙 ∈ ðŋ) → ðŋ <<s {(ðŋ |s 𝑅)})
254 simpr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑙 ∈ ðŋ) → 𝑙 ∈ ðŋ)
255 ovex 7391 . . . . . . . . . . . . . . . . . 18 (ðŋ |s 𝑅) ∈ V
256255snid 4623 . . . . . . . . . . . . . . . . 17 (ðŋ |s 𝑅) ∈ {(ðŋ |s 𝑅)}
257256a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑙 ∈ ðŋ) → (ðŋ |s 𝑅) ∈ {(ðŋ |s 𝑅)})
258253, 254, 257ssltsepcd 27136 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑙 ∈ ðŋ) → 𝑙 <s (ðŋ |s 𝑅))
2591adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑙 ∈ ðŋ) → ðī = (ðŋ |s 𝑅))
260258, 259breqtrrd 5134 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑙 ∈ ðŋ) → 𝑙 <s ðī)
2614adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑙 ∈ ðŋ) → ðī ∈ No )
262222, 261, 223sltadd1d 27310 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑙 ∈ ðŋ) → (𝑙 <s ðī ↔ (𝑙 +s ðĩ) <s (ðī +s ðĩ)))
263260, 262mpbid 231 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑙 ∈ ðŋ) → (𝑙 +s ðĩ) <s (ðī +s ðĩ))
264 breq1 5109 . . . . . . . . . . . . 13 (𝑎 = (𝑙 +s ðĩ) → (𝑎 <s (ðī +s ðĩ) ↔ (𝑙 +s ðĩ) <s (ðī +s ðĩ)))
265263, 264syl5ibrcom 247 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑙 ∈ ðŋ) → (𝑎 = (𝑙 +s ðĩ) → 𝑎 <s (ðī +s ðĩ)))
266265rexlimdva 3153 . . . . . . . . . . 11 (𝜑 → (∃𝑙 ∈ ðŋ 𝑎 = (𝑙 +s ðĩ) → 𝑎 <s (ðī +s ðĩ)))
267 scutcut 27143 . . . . . . . . . . . . . . . . . . 19 (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
2686, 267syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑀 |s 𝑆) ∈ No ∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆))
269268simp2d 1144 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑀 <<s {(𝑀 |s 𝑆)})
270269adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑀 <<s {(𝑀 |s 𝑆)})
271 simpr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 ∈ 𝑀)
272 ovex 7391 . . . . . . . . . . . . . . . . . 18 (𝑀 |s 𝑆) ∈ V
273272snid 4623 . . . . . . . . . . . . . . . . 17 (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)}
274273a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
275270, 271, 274ssltsepcd 27136 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s (𝑀 |s 𝑆))
2765adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑚 ∈ 𝑀) → ðĩ = (𝑀 |s 𝑆))
277275, 276breqtrrd 5134 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑚 ∈ 𝑀) → 𝑚 <s ðĩ)
2788adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑚 ∈ 𝑀) → ðĩ ∈ No )
279230, 278, 229sltadd2d 27309 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑚 <s ðĩ ↔ (ðī +s 𝑚) <s (ðī +s ðĩ)))
280277, 279mpbid 231 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑚 ∈ 𝑀) → (ðī +s 𝑚) <s (ðī +s ðĩ))
281 breq1 5109 . . . . . . . . . . . . 13 (𝑎 = (ðī +s 𝑚) → (𝑎 <s (ðī +s ðĩ) ↔ (ðī +s 𝑚) <s (ðī +s ðĩ)))
282280, 281syl5ibrcom 247 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑚 ∈ 𝑀) → (𝑎 = (ðī +s 𝑚) → 𝑎 <s (ðī +s ðĩ)))
283282rexlimdva 3153 . . . . . . . . . . 11 (𝜑 → (∃𝑚 ∈ 𝑀 𝑎 = (ðī +s 𝑚) → 𝑎 <s (ðī +s ðĩ)))
284266, 283jaod 858 . . . . . . . . . 10 (𝜑 → ((∃𝑙 ∈ ðŋ 𝑎 = (𝑙 +s ðĩ) âˆĻ ∃𝑚 ∈ 𝑀 𝑎 = (ðī +s 𝑚)) → 𝑎 <s (ðī +s ðĩ)))
285249, 284biimtrid 241 . . . . . . . . 9 (𝜑 → (𝑎 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) → 𝑎 <s (ðī +s ðĩ)))
286285imp 408 . . . . . . . 8 ((𝜑 ∧ 𝑎 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})) → 𝑎 <s (ðī +s ðĩ))
287 breq2 5110 . . . . . . . 8 (𝑏 = (ðī +s ðĩ) → (𝑎 <s 𝑏 ↔ 𝑎 <s (ðī +s ðĩ)))
288286, 287syl5ibrcom 247 . . . . . . 7 ((𝜑 ∧ 𝑎 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})) → (𝑏 = (ðī +s ðĩ) → 𝑎 <s 𝑏))
289239, 288biimtrid 241 . . . . . 6 ((𝜑 ∧ 𝑎 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)})) → (𝑏 ∈ {(ðī +s ðĩ)} → 𝑎 <s 𝑏))
2902893impia 1118 . . . . 5 ((𝜑 ∧ 𝑎 ∈ ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) ∧ 𝑏 ∈ {(ðī +s ðĩ)}) → 𝑎 <s 𝑏)
291219, 221, 236, 238, 290ssltd 27134 . . . 4 (𝜑 → ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) <<s {(ðī +s ðĩ)})
29210sneqd 4599 . . . 4 (𝜑 → {(ðī +s ðĩ)} = {(({𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)} ∊ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)}) |s ({𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)} ∊ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)}))})
293291, 292breqtrd 5132 . . 3 (𝜑 → ({ð‘Ķ âˆĢ ∃𝑙 ∈ ðŋ ð‘Ķ = (𝑙 +s ðĩ)} ∊ {𝑧 âˆĢ ∃𝑚 ∈ 𝑀 𝑧 = (ðī +s 𝑚)}) <<s {(({𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)} ∊ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)}) |s ({𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)} ∊ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)}))})
294 eqid 2737 . . . . . . . 8 (𝑟 ∈ 𝑅 â†Ķ (𝑟 +s ðĩ)) = (𝑟 ∈ 𝑅 â†Ķ (𝑟 +s ðĩ))
295294rnmpt 5911 . . . . . . 7 ran (𝑟 ∈ 𝑅 â†Ķ (𝑟 +s ðĩ)) = {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)}
296 ssltex2 27130 . . . . . . . . . 10 (ðŋ <<s 𝑅 → 𝑅 ∈ V)
2972, 296syl 17 . . . . . . . . 9 (𝜑 → 𝑅 ∈ V)
298297mptexd 7175 . . . . . . . 8 (𝜑 → (𝑟 ∈ 𝑅 â†Ķ (𝑟 +s ðĩ)) ∈ V)
299 rnexg 7842 . . . . . . . 8 ((𝑟 ∈ 𝑅 â†Ķ (𝑟 +s ðĩ)) ∈ V → ran (𝑟 ∈ 𝑅 â†Ķ (𝑟 +s ðĩ)) ∈ V)
300298, 299syl 17 . . . . . . 7 (𝜑 → ran (𝑟 ∈ 𝑅 â†Ķ (𝑟 +s ðĩ)) ∈ V)
301295, 300eqeltrrid 2843 . . . . . 6 (𝜑 → {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∈ V)
302 eqid 2737 . . . . . . . 8 (𝑠 ∈ 𝑆 â†Ķ (ðī +s 𝑠)) = (𝑠 ∈ 𝑆 â†Ķ (ðī +s 𝑠))
303302rnmpt 5911 . . . . . . 7 ran (𝑠 ∈ 𝑆 â†Ķ (ðī +s 𝑠)) = {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}
304 ssltex2 27130 . . . . . . . . . 10 (𝑀 <<s 𝑆 → 𝑆 ∈ V)
3056, 304syl 17 . . . . . . . . 9 (𝜑 → 𝑆 ∈ V)
306305mptexd 7175 . . . . . . . 8 (𝜑 → (𝑠 ∈ 𝑆 â†Ķ (ðī +s 𝑠)) ∈ V)
307 rnexg 7842 . . . . . . . 8 ((𝑠 ∈ 𝑆 â†Ķ (ðī +s 𝑠)) ∈ V → ran (𝑠 ∈ 𝑆 â†Ķ (ðī +s 𝑠)) ∈ V)
308306, 307syl 17 . . . . . . 7 (𝜑 → ran (𝑠 ∈ 𝑆 â†Ķ (ðī +s 𝑠)) ∈ V)
309303, 308eqeltrrid 2843 . . . . . 6 (𝜑 → {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)} ∈ V)
310301, 309unexd 7689 . . . . 5 (𝜑 → ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) ∈ V)
311113sselda 3945 . . . . . . . . . 10 ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ No )
3128adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑟 ∈ 𝑅) → ðĩ ∈ No )
313311, 312addscld 27293 . . . . . . . . 9 ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑟 +s ðĩ) ∈ No )
314 eleq1 2826 . . . . . . . . 9 (ð‘Ī = (𝑟 +s ðĩ) → (ð‘Ī ∈ No ↔ (𝑟 +s ðĩ) ∈ No ))
315313, 314syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ 𝑟 ∈ 𝑅) → (ð‘Ī = (𝑟 +s ðĩ) → ð‘Ī ∈ No ))
316315rexlimdva 3153 . . . . . . 7 (𝜑 → (∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ) → ð‘Ī ∈ No ))
317316abssdv 4026 . . . . . 6 (𝜑 → {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ⊆ No )
3184adantr 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑠 ∈ 𝑆) → ðī ∈ No )
319144sselda 3945 . . . . . . . . . 10 ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ No )
320318, 319addscld 27293 . . . . . . . . 9 ((𝜑 ∧ 𝑠 ∈ 𝑆) → (ðī +s 𝑠) ∈ No )
321 eleq1 2826 . . . . . . . . 9 (ð‘Ą = (ðī +s 𝑠) → (ð‘Ą ∈ No ↔ (ðī +s 𝑠) ∈ No ))
322320, 321syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ 𝑠 ∈ 𝑆) → (ð‘Ą = (ðī +s 𝑠) → ð‘Ą ∈ No ))
323322rexlimdva 3153 . . . . . . 7 (𝜑 → (∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠) → ð‘Ą ∈ No ))
324323abssdv 4026 . . . . . 6 (𝜑 → {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)} ⊆ No )
325317, 324unssd 4147 . . . . 5 (𝜑 → ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) ⊆ No )
326 velsn 4603 . . . . . . 7 (𝑎 ∈ {(ðī +s ðĩ)} ↔ 𝑎 = (ðī +s ðĩ))
327 elun 4109 . . . . . . . . . . . . 13 (𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) ↔ (𝑏 ∈ {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} âˆĻ 𝑏 ∈ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}))
328 vex 3450 . . . . . . . . . . . . . . 15 𝑏 ∈ V
329328, 125elab 3631 . . . . . . . . . . . . . 14 (𝑏 ∈ {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ↔ ∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ))
330328, 156elab 3631 . . . . . . . . . . . . . 14 (𝑏 ∈ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)} ↔ ∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠))
331329, 330orbi12i 914 . . . . . . . . . . . . 13 ((𝑏 ∈ {ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} âˆĻ 𝑏 ∈ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ) âˆĻ ∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠)))
332327, 331bitri 275 . . . . . . . . . . . 12 (𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) ↔ (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ) âˆĻ ∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠)))
3331adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑟 ∈ 𝑅) → ðī = (ðŋ |s 𝑅))
334251simp3d 1145 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {(ðŋ |s 𝑅)} <<s 𝑅)
335334adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑟 ∈ 𝑅) → {(ðŋ |s 𝑅)} <<s 𝑅)
336256a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑟 ∈ 𝑅) → (ðŋ |s 𝑅) ∈ {(ðŋ |s 𝑅)})
337 simpr 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ 𝑅)
338335, 336, 337ssltsepcd 27136 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑟 ∈ 𝑅) → (ðŋ |s 𝑅) <s 𝑟)
339333, 338eqbrtrd 5128 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑟 ∈ 𝑅) → ðī <s 𝑟)
3404adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑟 ∈ 𝑅) → ðī ∈ No )
341340, 311, 312sltadd1d 27310 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑟 ∈ 𝑅) → (ðī <s 𝑟 ↔ (ðī +s ðĩ) <s (𝑟 +s ðĩ)))
342339, 341mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑟 ∈ 𝑅) → (ðī +s ðĩ) <s (𝑟 +s ðĩ))
343 breq2 5110 . . . . . . . . . . . . . . 15 (𝑏 = (𝑟 +s ðĩ) → ((ðī +s ðĩ) <s 𝑏 ↔ (ðī +s ðĩ) <s (𝑟 +s ðĩ)))
344342, 343syl5ibrcom 247 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝑏 = (𝑟 +s ðĩ) → (ðī +s ðĩ) <s 𝑏))
345344rexlimdva 3153 . . . . . . . . . . . . 13 (𝜑 → (∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ) → (ðī +s ðĩ) <s 𝑏))
3465adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑠 ∈ 𝑆) → ðĩ = (𝑀 |s 𝑆))
347268simp3d 1145 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {(𝑀 |s 𝑆)} <<s 𝑆)
348347adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑠 ∈ 𝑆) → {(𝑀 |s 𝑆)} <<s 𝑆)
349273a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)})
350 simpr 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
351348, 349, 350ssltsepcd 27136 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑀 |s 𝑆) <s 𝑠)
352346, 351eqbrtrd 5128 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑠 ∈ 𝑆) → ðĩ <s 𝑠)
3538adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑠 ∈ 𝑆) → ðĩ ∈ No )
354353, 319, 318sltadd2d 27309 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑠 ∈ 𝑆) → (ðĩ <s 𝑠 ↔ (ðī +s ðĩ) <s (ðī +s 𝑠)))
355352, 354mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑠 ∈ 𝑆) → (ðī +s ðĩ) <s (ðī +s 𝑠))
356 breq2 5110 . . . . . . . . . . . . . . 15 (𝑏 = (ðī +s 𝑠) → ((ðī +s ðĩ) <s 𝑏 ↔ (ðī +s ðĩ) <s (ðī +s 𝑠)))
357355, 356syl5ibrcom 247 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑏 = (ðī +s 𝑠) → (ðī +s ðĩ) <s 𝑏))
358357rexlimdva 3153 . . . . . . . . . . . . 13 (𝜑 → (∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠) → (ðī +s ðĩ) <s 𝑏))
359345, 358jaod 858 . . . . . . . . . . . 12 (𝜑 → ((∃𝑟 ∈ 𝑅 𝑏 = (𝑟 +s ðĩ) âˆĻ ∃𝑠 ∈ 𝑆 𝑏 = (ðī +s 𝑠)) → (ðī +s ðĩ) <s 𝑏))
360332, 359biimtrid 241 . . . . . . . . . . 11 (𝜑 → (𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) → (ðī +s ðĩ) <s 𝑏))
361360imp 408 . . . . . . . . . 10 ((𝜑 ∧ 𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})) → (ðī +s ðĩ) <s 𝑏)
362 breq1 5109 . . . . . . . . . 10 (𝑎 = (ðī +s ðĩ) → (𝑎 <s 𝑏 ↔ (ðī +s ðĩ) <s 𝑏))
363361, 362syl5ibrcom 247 . . . . . . . . 9 ((𝜑 ∧ 𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})) → (𝑎 = (ðī +s ðĩ) → 𝑎 <s 𝑏))
364363ex 414 . . . . . . . 8 (𝜑 → (𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) → (𝑎 = (ðī +s ðĩ) → 𝑎 <s 𝑏)))
365364com23 86 . . . . . . 7 (𝜑 → (𝑎 = (ðī +s ðĩ) → (𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) → 𝑎 <s 𝑏)))
366326, 365biimtrid 241 . . . . . 6 (𝜑 → (𝑎 ∈ {(ðī +s ðĩ)} → (𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}) → 𝑎 <s 𝑏)))
3673663imp 1112 . . . . 5 ((𝜑 ∧ 𝑎 ∈ {(ðī +s ðĩ)} ∧ 𝑏 ∈ ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)})) → 𝑎 <s 𝑏)
368221, 310, 238, 325, 367ssltd 27134 . . . 4 (𝜑 → {(ðī +s ðĩ)} <<s ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}))
369292, 368eqbrtrrd 5130 . . 3 (𝜑 → {(({𝑎 âˆĢ ∃𝑝 ∈ ( L ‘ðī)𝑎 = (𝑝 +s ðĩ)} ∊ {𝑏 âˆĢ ∃𝑞 ∈ ( L ‘ðĩ)𝑏 = (ðī +s 𝑞)}) |s ({𝑐 âˆĢ ∃𝑒 ∈ ( R ‘ðī)𝑐 = (𝑒 +s ðĩ)} ∊ {𝑑 âˆĢ ∃𝑓 ∈ ( R ‘ðĩ)𝑑 = (ðī +s 𝑓)}))} <<s ({ð‘Ī âˆĢ ∃𝑟 ∈ 𝑅 ð‘Ī = (𝑟 +s ðĩ)} ∊ {ð‘Ą âˆĢ ∃𝑠 ∈ 𝑆 ð‘Ą = (ðī +s 𝑠)}))
37018, 110, 202, 293, 369cofcut1d 27243 . 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 397   âˆĻ wo 846   ∧ w3a 1088  âˆ€wal 1540   = wceq 1542  âˆƒwex 1782   ∈ wcel 2107  {cab 2714   ≠ wne 2944  âˆ€wral 3065  âˆƒwrex 3074  Vcvv 3446   ∊ cun 3909   ⊆ wss 3911  âˆ…c0 4283  {csn 4587   class class class wbr 5106   â†Ķ cmpt 5189  ran crn 5635  â€˜cfv 6497  (class class class)co 7358   No csur 26991   <s cslt 26992   â‰Īs csle 27095   <<s csslt 27123   |s cscut 27125   L cleft 27178   R cright 27179   +s cadds 27274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-ot 4596  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-1o 8413  df-2o 8414  df-nadd 8613  df-no 26994  df-slt 26995  df-bday 26996  df-sle 27096  df-sslt 27124  df-scut 27126  df-0s 27166  df-made 27180  df-old 27181  df-left 27183  df-right 27184  df-norec2 27264  df-adds 27275
This theorem is referenced by:  addsasslem1  27314  addsasslem2  27315  negsid  27342
  Copyright terms: Public domain W3C validator