Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  caucvgprlemladdrl Structured version   GIF version

 Description: Lemma for caucvgpr 6653. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.)
Hypotheses
Ref Expression
caucvgpr.f (φ𝐹:NQ)
caucvgpr.cau (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
caucvgpr.bnd (φ𝑗 N A <Q (𝐹𝑗))
caucvgpr.lim 𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩
Assertion
Ref Expression
caucvgprlemladdrl (φ → {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
Distinct variable groups:   A,𝑗   𝑗,𝐹,u,𝑙   𝑛,𝐹,𝑘   𝑘,𝐿,𝑗   𝑆,𝑙,u,𝑗   𝑗,𝑘,𝑆
Allowed substitution hints:   φ(u,𝑗,𝑘,𝑛,𝑙)   A(u,𝑘,𝑛,𝑙)   𝑆(𝑛)   𝐿(u,𝑛,𝑙)

Proof of Theorem caucvgprlemladdrl
Dummy variables 𝑟 f g 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 3540 . . . . . . . . 9 (𝑗 = 𝑎 → ⟨𝑗, 1𝑜⟩ = ⟨𝑎, 1𝑜⟩)
21eceq1d 6078 . . . . . . . 8 (𝑗 = 𝑎 → [⟨𝑗, 1𝑜⟩] ~Q = [⟨𝑎, 1𝑜⟩] ~Q )
32fveq2d 5125 . . . . . . 7 (𝑗 = 𝑎 → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))
43oveq2d 5471 . . . . . 6 (𝑗 = 𝑎 → (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) = (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )))
5 fveq2 5121 . . . . . . 7 (𝑗 = 𝑎 → (𝐹𝑗) = (𝐹𝑎))
65oveq1d 5470 . . . . . 6 (𝑗 = 𝑎 → ((𝐹𝑗) +Q 𝑆) = ((𝐹𝑎) +Q 𝑆))
74, 6breq12d 3768 . . . . 5 (𝑗 = 𝑎 → ((𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆) ↔ (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
87cbvrexv 2528 . . . 4 (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆) ↔ 𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆))
98a1i 9 . . 3 (𝑙 Q → (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆) ↔ 𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
109rabbiia 2541 . 2 {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆)} = {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)}
11 oveq1 5462 . . . . . . 7 (𝑙 = 𝑟 → (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )))
1211breq1d 3765 . . . . . 6 (𝑙 = 𝑟 → ((𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) ↔ (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
1312rexbidv 2321 . . . . 5 (𝑙 = 𝑟 → (𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) ↔ 𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
1413elrab 2692 . . . 4 (𝑟 {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)} ↔ (𝑟 Q 𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
15 caucvgpr.f . . . . . . . . . . . . . . 15 (φ𝐹:NQ)
1615ad4antr 463 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝐹:NQ)
17 caucvgpr.cau . . . . . . . . . . . . . . 15 (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
1817ad4antr 463 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
19 simpr 103 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑏 N)
20 simpllr 486 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑎 N)
2116, 18, 19, 20caucvgprlemnbj 6638 . . . . . . . . . . . . 13 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ¬ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q (𝐹𝑎))
2215ad3antrrr 461 . . . . . . . . . . . . . . . . . 18 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝐹:NQ)
2322ffvelrnda 5245 . . . . . . . . . . . . . . . . 17 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (𝐹𝑏) Q)
24 nnnq 6405 . . . . . . . . . . . . . . . . . 18 (𝑏 N → [⟨𝑏, 1𝑜⟩] ~Q Q)
25 recclnq 6376 . . . . . . . . . . . . . . . . . 18 ([⟨𝑏, 1𝑜⟩] ~Q Q → (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) Q)
2619, 24, 253syl 17 . . . . . . . . . . . . . . . . 17 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) Q)
27 addclnq 6359 . . . . . . . . . . . . . . . . 17 (((𝐹𝑏) Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) Q) → ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q)
2823, 26, 27syl2anc 391 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q)
29 nnnq 6405 . . . . . . . . . . . . . . . . 17 (𝑎 N → [⟨𝑎, 1𝑜⟩] ~Q Q)
30 recclnq 6376 . . . . . . . . . . . . . . . . 17 ([⟨𝑎, 1𝑜⟩] ~Q Q → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
3120, 29, 303syl 17 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
32 caucvgprlemladd.s . . . . . . . . . . . . . . . . 17 (φ𝑆 Q)
3332ad4antr 463 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑆 Q)
34 addassnqg 6366 . . . . . . . . . . . . . . . 16 ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q 𝑆 Q) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) = (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)))
3528, 31, 33, 34syl3anc 1134 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) = (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)))
3635breq1d 3765 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) <Q ((𝐹𝑎) +Q 𝑆) ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)) <Q ((𝐹𝑎) +Q 𝑆)))
37 ltanqg 6384 . . . . . . . . . . . . . . . 16 ((f Q g Q Q) → (f <Q g ↔ ( +Q f) <Q ( +Q g)))
3837adantl 262 . . . . . . . . . . . . . . 15 ((((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) (f Q g Q Q)) → (f <Q g ↔ ( +Q f) <Q ( +Q g)))
39 addclnq 6359 . . . . . . . . . . . . . . . 16 ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q) → (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
4028, 31, 39syl2anc 391 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
4116, 20ffvelrnd 5246 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (𝐹𝑎) Q)
42 addcomnqg 6365 . . . . . . . . . . . . . . . 16 ((f Q g Q) → (f +Q g) = (g +Q f))
4342adantl 262 . . . . . . . . . . . . . . 15 ((((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) (f Q g Q)) → (f +Q g) = (g +Q f))
4438, 40, 41, 33, 43caovord2d 5612 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q (𝐹𝑎) ↔ ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) <Q ((𝐹𝑎) +Q 𝑆)))
45 addcomnqg 6365 . . . . . . . . . . . . . . . . 17 ((𝑆 Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆))
4633, 31, 45syl2anc 391 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆))
4746oveq2d 5471 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) = (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)))
4847breq1d 3765 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆) ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)) <Q ((𝐹𝑎) +Q 𝑆)))
4936, 44, 483bitr4rd 210 . . . . . . . . . . . . 13 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆) ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q (𝐹𝑎)))
5021, 49mtbird 597 . . . . . . . . . . . 12 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ¬ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆))
5150nrexdv 2406 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ¬ 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆))
5251intnand 839 . . . . . . . . . 10 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ¬ (((𝐹𝑎) +Q 𝑆) Q 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
5317ad3antrrr 461 . . . . . . . . . . . . 13 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
54 caucvgpr.bnd . . . . . . . . . . . . . . 15 (φ𝑗 N A <Q (𝐹𝑗))
55 fveq2 5121 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑏 → (𝐹𝑗) = (𝐹𝑏))
5655breq2d 3767 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑏 → (A <Q (𝐹𝑗) ↔ A <Q (𝐹𝑏)))
5756cbvralv 2527 . . . . . . . . . . . . . . 15 (𝑗 N A <Q (𝐹𝑗) ↔ 𝑏 N A <Q (𝐹𝑏))
5854, 57sylib 127 . . . . . . . . . . . . . 14 (φ𝑏 N A <Q (𝐹𝑏))
5958ad3antrrr 461 . . . . . . . . . . . . 13 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑏 N A <Q (𝐹𝑏))
60 caucvgpr.lim . . . . . . . . . . . . . 14 𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩
61 opeq1 3540 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑏 → ⟨𝑗, 1𝑜⟩ = ⟨𝑏, 1𝑜⟩)
6261eceq1d 6078 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑏 → [⟨𝑗, 1𝑜⟩] ~Q = [⟨𝑏, 1𝑜⟩] ~Q )
6362fveq2d 5125 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑏 → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))
6463oveq2d 5471 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑏 → (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) = (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
6564, 55breq12d 3768 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑏 → ((𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗) ↔ (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)))
6665cbvrexv 2528 . . . . . . . . . . . . . . . . 17 (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗) ↔ 𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏))
6766a1i 9 . . . . . . . . . . . . . . . 16 (𝑙 Q → (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗) ↔ 𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)))
6867rabbiia 2541 . . . . . . . . . . . . . . 15 {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)} = {𝑙 Q𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)}
6955, 63oveq12d 5473 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑏 → ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) = ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
7069breq1d 3765 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑏 → (((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u ↔ ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u))
7170cbvrexv 2528 . . . . . . . . . . . . . . . . 17 (𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u)
7271a1i 9 . . . . . . . . . . . . . . . 16 (u Q → (𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u))
7372rabbiia 2541 . . . . . . . . . . . . . . 15 {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u} = {u Q𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u}
7468, 73opeq12i 3545 . . . . . . . . . . . . . 14 ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩ = ⟨{𝑙 Q𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)}, {u Q𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u}⟩
7560, 74eqtri 2057 . . . . . . . . . . . . 13 𝐿 = ⟨{𝑙 Q𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)}, {u Q𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u}⟩
7632ad3antrrr 461 . . . . . . . . . . . . . 14 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑆 Q)
7729, 30syl 14 . . . . . . . . . . . . . . 15 (𝑎 N → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
7877ad2antlr 458 . . . . . . . . . . . . . 14 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
79 addclnq 6359 . . . . . . . . . . . . . 14 ((𝑆 Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
8076, 78, 79syl2anc 391 . . . . . . . . . . . . 13 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
8122, 53, 59, 75, 80caucvgprlemladdfu 6648 . . . . . . . . . . . 12 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ⊆ {u Q𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u})
8281sseld 2938 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) → ((𝐹𝑎) +Q 𝑆) {u Q𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u}))
83 breq2 3759 . . . . . . . . . . . . 13 (u = ((𝐹𝑎) +Q 𝑆) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
8483rexbidv 2321 . . . . . . . . . . . 12 (u = ((𝐹𝑎) +Q 𝑆) → (𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
8584elrab 2692 . . . . . . . . . . 11 (((𝐹𝑎) +Q 𝑆) {u Q𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u} ↔ (((𝐹𝑎) +Q 𝑆) Q 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
8682, 85syl6ib 150 . . . . . . . . . 10 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) → (((𝐹𝑎) +Q 𝑆) Q 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆))))
8752, 86mtod 588 . . . . . . . . 9 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ¬ ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)))
8815, 17, 54, 60caucvgprlemcl 6647 . . . . . . . . . . . 12 (φ𝐿 P)
8988ad3antrrr 461 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝐿 P)
90 nqprlu 6530 . . . . . . . . . . . 12 ((𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q → ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩ P)
9180, 90syl 14 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩ P)
92 addclpr 6520 . . . . . . . . . . 11 ((𝐿 P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩ P) → (𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P)
9389, 91, 92syl2anc 391 . . . . . . . . . 10 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P)
94 prop 6458 . . . . . . . . . . 11 ((𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P → ⟨(1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)), (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))⟩ P)
95 prloc 6474 . . . . . . . . . . 11 ((⟨(1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)), (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))⟩ P (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))))
9694, 95sylan 267 . . . . . . . . . 10 (((𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))))
9793, 96sylancom 397 . . . . . . . . 9 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))))
9887, 97ecased 1238 . . . . . . . 8 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)))
99 simpllr 486 . . . . . . . . 9 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑟 Q)
10089, 76, 99, 78cauappcvgprlemcan 6616 . . . . . . . 8 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ↔ 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
10198, 100mpbid 135 . . . . . . 7 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
102101ex 108 . . . . . 6 (((φ 𝑟 Q) 𝑎 N) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
103102rexlimdva 2427 . . . . 5 ((φ 𝑟 Q) → (𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
104103expimpd 345 . . . 4 (φ → ((𝑟 Q 𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
10514, 104syl5bi 141 . . 3 (φ → (𝑟 {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)} → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
106105ssrdv 2945 . 2 (φ → {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
10710, 106syl5eqss 2983 1 (φ → {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301  {crab 2304   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755  ⟶wf 4841  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  1𝑜c1o 5933  [cec 6040  Ncnpi 6256
 Copyright terms: Public domain W3C validator