Theorem cauappcvgprlemladdfu 7404

Description: Lemma for cauappcvgprlemladd 7408. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)

Hypotheses

Ref	Expression
cauappcvgpr.f	⊢ (𝜑 → 𝐹:Q⟶Q)
cauappcvgpr.app	⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))))
cauappcvgpr.bnd	⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝))
cauappcvgpr.lim	⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩
cauappcvgprlemladd.s	⊢ (𝜑 → 𝑆 ∈ Q)

Assertion

Ref	Expression
cauappcvgprlemladdfu	⊢ (𝜑 → (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) ⊆ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩))

Distinct variable groups:   𝐴,𝑝   𝐿,𝑝,𝑞   𝜑,𝑝,𝑞   𝐹,𝑙,𝑢,𝑝,𝑞   𝑆,𝑙,𝑞,𝑢

Allowed substitution hints:   𝜑(𝑢,𝑙)   𝐴(𝑢,𝑞,𝑙)   𝑆(𝑝)   𝐿(𝑢,𝑙)

Proof of Theorem cauappcvgprlemladdfu

Dummy variables 𝑓 𝑔 ℎ 𝑟 𝑠 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cauappcvgpr.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:Q⟶Q)
2		cauappcvgpr.app	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))))
3		cauappcvgpr.bnd	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝))
4		cauappcvgpr.lim	. . . . . . 7 ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩
5	1, 2, 3, 4	cauappcvgprlemcl 7403	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ P)
6		cauappcvgprlemladd.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Q)
7		nqprlu 7297	. . . . . . 7 ⊢ (𝑆 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩ ∈ P)
8	6, 7	syl 14	. . . . . 6 ⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩ ∈ P)
9		df-iplp 7218	. . . . . . 7 ⊢ +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑓 ∈ Q ∣ ∃𝑔 ∈ Q ∃ℎ ∈ Q (𝑔 ∈ (1st ‘𝑥) ∧ ℎ ∈ (1st ‘𝑦) ∧ 𝑓 = (𝑔 +Q ℎ))}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ Q ∃ℎ ∈ Q (𝑔 ∈ (2nd ‘𝑥) ∧ ℎ ∈ (2nd ‘𝑦) ∧ 𝑓 = (𝑔 +Q ℎ))}⟩)
10		addclnq 7125	. . . . . . 7 ⊢ ((𝑔 ∈ Q ∧ ℎ ∈ Q) → (𝑔 +Q ℎ) ∈ Q)
11	9, 10	genpelvu 7263	. . . . . 6 ⊢ ((𝐿 ∈ P ∧ ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩ ∈ P) → (𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) ↔ ∃𝑠 ∈ (2nd ‘𝐿)∃𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)𝑟 = (𝑠 +Q 𝑡)))
12	5, 8, 11	syl2anc 406	. . . . 5 ⊢ (𝜑 → (𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) ↔ ∃𝑠 ∈ (2nd ‘𝐿)∃𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)𝑟 = (𝑠 +Q 𝑡)))
13	12	biimpa 292	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) → ∃𝑠 ∈ (2nd ‘𝐿)∃𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)𝑟 = (𝑠 +Q 𝑡))
14		breq2 3897	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑠 → (((𝐹‘𝑞) +Q 𝑞) <Q 𝑢 ↔ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠))
15	14	rexbidv 2410	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑠 → (∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢 ↔ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠))
16	4	fveq2i 5376	. . . . . . . . . . . . . . . 16 ⊢ (2nd ‘𝐿) = (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩)
17		nqex 7113	. . . . . . . . . . . . . . . . . 18 ⊢ Q ∈ V
18	17	rabex 4030	. . . . . . . . . . . . . . . . 17 ⊢ {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)} ∈ V
19	17	rabex 4030	. . . . . . . . . . . . . . . . 17 ⊢ {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢} ∈ V
20	18, 19	op2nd 5997	. . . . . . . . . . . . . . . 16 ⊢ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩) = {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}
21	16, 20	eqtri 2133	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}
22	15, 21	elrab2 2810	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (2nd ‘𝐿) ↔ (𝑠 ∈ Q ∧ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠))
23	22	biimpi 119	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (2nd ‘𝐿) → (𝑠 ∈ Q ∧ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠))
24	23	adantr 272	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) → (𝑠 ∈ Q ∧ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠))
25	24	adantl 273	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) → (𝑠 ∈ Q ∧ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠))
26	25	adantr 272	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑠 ∈ Q ∧ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠))
27	26	simpld 111	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑠 ∈ Q)
28		vex 2658	. . . . . . . . . . . . . 14 ⊢ 𝑡 ∈ V
29		breq2 3897	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → (𝑆 <Q 𝑢 ↔ 𝑆 <Q 𝑡))
30		ltnqex 7299	. . . . . . . . . . . . . . 15 ⊢ {𝑙 ∣ 𝑙 <Q 𝑆} ∈ V
31		gtnqex 7300	. . . . . . . . . . . . . . 15 ⊢ {𝑢 ∣ 𝑆 <Q 𝑢} ∈ V
32	30, 31	op2nd 5997	. . . . . . . . . . . . . 14 ⊢ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩) = {𝑢 ∣ 𝑆 <Q 𝑢}
33	28, 29, 32	elab2 2799	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩) ↔ 𝑆 <Q 𝑡)
34		ltrelnq 7115	. . . . . . . . . . . . . 14 ⊢ <Q ⊆ (Q × Q)
35	34	brel 4549	. . . . . . . . . . . . 13 ⊢ (𝑆 <Q 𝑡 → (𝑆 ∈ Q ∧ 𝑡 ∈ Q))
36	33, 35	sylbi 120	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩) → (𝑆 ∈ Q ∧ 𝑡 ∈ Q))
37	36	simprd 113	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩) → 𝑡 ∈ Q)
38	37	ad2antll 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) → 𝑡 ∈ Q)
39	38	adantr 272	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑡 ∈ Q)
40		addclnq 7125	. . . . . . . . 9 ⊢ ((𝑠 ∈ Q ∧ 𝑡 ∈ Q) → (𝑠 +Q 𝑡) ∈ Q)
41	27, 39, 40	syl2anc 406	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑠 +Q 𝑡) ∈ Q)
42		eleq1 2175	. . . . . . . . 9 ⊢ (𝑟 = (𝑠 +Q 𝑡) → (𝑟 ∈ Q ↔ (𝑠 +Q 𝑡) ∈ Q))
43	42	adantl 273	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑟 ∈ Q ↔ (𝑠 +Q 𝑡) ∈ Q))
44	41, 43	mpbird 166	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑟 ∈ Q)
45	26	simprd 113	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠)
46	33	biimpi 119	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩) → 𝑆 <Q 𝑡)
47	46	ad2antll 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) → 𝑆 <Q 𝑡)
48	47	adantr 272	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑆 <Q 𝑡)
49	48	ad2antrr 477	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → 𝑆 <Q 𝑡)
50	6	ad5antr 485	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → 𝑆 ∈ Q)
51	39	ad2antrr 477	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → 𝑡 ∈ Q)
52	1	ad5antr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → 𝐹:Q⟶Q)
53		simplr 502	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → 𝑞 ∈ Q)
54	52, 53	ffvelrnd 5508	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → (𝐹‘𝑞) ∈ Q)
55		addclnq 7125	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑞) ∈ Q ∧ 𝑞 ∈ Q) → ((𝐹‘𝑞) +Q 𝑞) ∈ Q)
56	54, 53, 55	syl2anc 406	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → ((𝐹‘𝑞) +Q 𝑞) ∈ Q)
57		ltanqg 7150	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ Q ∧ 𝑡 ∈ Q ∧ ((𝐹‘𝑞) +Q 𝑞) ∈ Q) → (𝑆 <Q 𝑡 ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑡)))
58	50, 51, 56, 57	syl3anc 1197	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → (𝑆 <Q 𝑡 ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑡)))
59	49, 58	mpbid 146	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑡))
60		simpr 109	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠)
61		ltanqg 7150	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → (𝑓 <Q 𝑔 ↔ (ℎ +Q 𝑓) <Q (ℎ +Q 𝑔)))
62	61	adantl 273	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q)) → (𝑓 <Q 𝑔 ↔ (ℎ +Q 𝑓) <Q (ℎ +Q 𝑔)))
63	27	ad2antrr 477	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → 𝑠 ∈ Q)
64		addcomnqg 7131	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
65	64	adantl 273	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q)) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
66	62, 56, 63, 51, 65	caovord2d 5892	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → (((𝐹‘𝑞) +Q 𝑞) <Q 𝑠 ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑡) <Q (𝑠 +Q 𝑡)))
67	60, 66	mpbid 146	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑡) <Q (𝑠 +Q 𝑡))
68		ltsonq 7148	. . . . . . . . . . . . 13 ⊢ <Q Or Q
69	68, 34	sotri 4890	. . . . . . . . . . . 12 ⊢ (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑡) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑡) <Q (𝑠 +Q 𝑡)) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q (𝑠 +Q 𝑡))
70	59, 67, 69	syl2anc 406	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q (𝑠 +Q 𝑡))
71		simpllr 506	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → 𝑟 = (𝑠 +Q 𝑡))
72	70, 71	breqtrrd 3919	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) ∧ ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟)
73	72	ex 114	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) ∧ 𝑞 ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) <Q 𝑠 → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
74	73	reximdva 2506	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑠 → ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
75	45, 74	mpd 13	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟)
76		breq2 3897	. . . . . . . . 9 ⊢ (𝑢 = 𝑟 → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢 ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
77	76	rexbidv 2410	. . . . . . . 8 ⊢ (𝑢 = 𝑟 → (∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢 ↔ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
78	17	rabex 4030	. . . . . . . . 9 ⊢ {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)} ∈ V
79	17	rabex 4030	. . . . . . . . 9 ⊢ {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢} ∈ V
80	78, 79	op2nd 5997	. . . . . . . 8 ⊢ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩) = {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}
81	77, 80	elrab2 2810	. . . . . . 7 ⊢ (𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩) ↔ (𝑟 ∈ Q ∧ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
82	44, 75, 81	sylanbrc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩))
83	82	ex 114	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) ∧ (𝑠 ∈ (2nd ‘𝐿) ∧ 𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) → (𝑟 = (𝑠 +Q 𝑡) → 𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩)))
84	83	rexlimdvva 2529	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) → (∃𝑠 ∈ (2nd ‘𝐿)∃𝑡 ∈ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)𝑟 = (𝑠 +Q 𝑡) → 𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩)))
85	13, 84	mpd 13	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) → 𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩))
86	85	ex 114	. 2 ⊢ (𝜑 → (𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) → 𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩)))
87	86	ssrdv 3067	1 ⊢ (𝜑 → (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) ⊆ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 943   = wceq 1312   ∈ wcel 1461  {cab 2099  ∀wral 2388  ∃wrex 2389  {crab 2392   ⊆ wss 3035  ⟨cop 3494   class class class wbr 3893  ⟶wf 5075  ‘cfv 5079  (class class class)co 5726  2^nd c2nd 5989  Qcnq 7030   +_Q cplq 7032   <_Q cltq 7035  Pcnp 7041   +_P cpp 7043

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460

This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-eprel 4169  df-id 4173  df-po 4176  df-iso 4177  df-iord 4246  df-on 4248  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-ov 5729  df-oprab 5730  df-mpo 5731  df-1st 5990  df-2nd 5991  df-recs 6154  df-irdg 6219  df-1o 6265  df-oadd 6269  df-omul 6270  df-er 6381  df-ec 6383  df-qs 6387  df-ni 7054  df-pli 7055  df-mi 7056  df-lti 7057  df-plpq 7094  df-mpq 7095  df-enq 7097  df-nqqs 7098  df-plqqs 7099  df-mqqs 7100  df-1nqqs 7101  df-rq 7102  df-ltnqqs 7103  df-inp 7216  df-iplp 7218

This theorem is referenced by:  cauappcvgprlemladdrl  7407  cauappcvgprlemladd  7408