smfaddlem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > smfaddlem1		Structured version Visualization version GIF version

Theorem smfaddlem1 47301

Description: Given the sum of two functions, the preimage of an unbounded below, open interval, expressed as the countable union of intersections of preimages of both functions. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)

**Hypotheses**
Ref	Expression
smfaddlem1.x	⊢ Ⅎ𝑥𝜑
smfaddlem1.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
smfaddlem1.d	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)
smfaddlem1.r	⊢ (𝜑 → 𝑅 ∈ ℝ)
smfaddlem1.k	⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})

**Assertion**
Ref	Expression
smfaddlem1	⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})

Distinct variable groups: 𝐴,𝑝,𝑞 𝐵,𝑝,𝑞 𝐶,𝑝,𝑞 𝐷,𝑝,𝑞 𝑥,𝐾 𝑅,𝑝,𝑞 𝜑,𝑝,𝑞 𝑥,𝑝,𝑞 Allowed substitution hints: 𝜑(𝑥) 𝐴(𝑥) 𝐵(𝑥) 𝐶(𝑥) 𝐷(𝑥) 𝑅(𝑥) 𝐾(𝑞,𝑝)

**Proof of Theorem smfaddlem1**
Step	Hyp	Ref	Expression
1		smfaddlem1.x	. . 3 ⊢ Ⅎ𝑥𝜑
2		simpl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝜑)
3		inss1 4188	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ 𝐶) ⊆ 𝐴
4		rabid 3434	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
5	4	simplbi 500	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ (𝐴 ∩ 𝐶))
6	3, 5	sselid 3934	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ 𝐴)
7	6	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ 𝐴)
8		smfaddlem1.b	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	2, 7, 8	syl2anc 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ)
10	9	rexrd 11229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ^*)
11		smfaddlem1.r	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℝ)
12	11	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑅 ∈ ℝ)
13		elinel2 4154	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐶)
14	13	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐶)
15		smfaddlem1.d	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)
16	14, 15	syldan 600	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐷 ∈ ℝ)
17	5, 16	sylan2 602	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐷 ∈ ℝ)
18	12, 17	resubcld 11612	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ)
19	18	rexrd 11229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ^*)
20	4	simprbi 501	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → (𝐵 + 𝐷) < 𝑅)
21	20	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝐵 + 𝐷) < 𝑅)
22	9, 17, 12	ltaddsubd 11784	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ((𝐵 + 𝐷) < 𝑅 ↔ 𝐵 < (𝑅 − 𝐷)))
23	21, 22	mpbid 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 < (𝑅 − 𝐷))
24	10, 19, 23	qelioo 46086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
25	17	rexrd 11229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐷 ∈ ℝ^*)
26	25	ad2antrr 736	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 ∈ ℝ^*)
27	11	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑅 ∈ ℝ)
28		qre 12951	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℝ)
29	28	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℝ)
30	27, 29	resubcld 11612	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ)
31	30	rexrd 11229	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ^*)
32	31	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑅 − 𝑝) ∈ ℝ^*)
33		elioore 13376	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → 𝑝 ∈ ℝ)
34	33	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 ∈ ℝ)
35	12	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑅 ∈ ℝ)
36	17	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 ∈ ℝ)
37	10	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 ∈ ℝ^*)
38	19	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑅 − 𝐷) ∈ ℝ^*)
39		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
40		iooltub 46050	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
41	37, 38, 39, 40	syl3anc 1389	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
42	34, 35, 36, 41	ltsub13d 11790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
43	42	adantlr 725	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
44	26, 32, 43	qelioo 46086	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
45		nfv 1933	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞(((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
46		nfre1 3286	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
47		simplr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℚ)
48		elioore 13376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → 𝑞 ∈ ℝ)
49	48	3ad2ant3 1147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℝ)
50	35	3adant3 1144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℝ)
51	33	3ad2ant2 1146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℝ)
52	50, 51	resubcld 11612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ)
53	25	3ad2ant1 1145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
54	52	rexrd 11229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
55		simp3 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
56		iooltub 46050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
57	53, 54, 55, 56	syl3anc 1389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
58	49, 52, 51, 57	ltadd2dd 11339	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < (𝑝 + (𝑅 − 𝑝)))
59	51	recnd 11207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℂ)
60	50	recnd 11207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℂ)
61	59, 60	pncan3d 11542	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + (𝑅 − 𝑝)) = 𝑅)
62	58, 61	breqtrd 5125	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
63	62	ad5ant135 1385	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
64	47, 63	jca 519	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
65		rabid 3434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ↔ (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
66	64, 65	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
67		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℚ)
68		qex 12959	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ ∈ V
69	68	rabex 5294	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V
70	69	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V)
71		smfaddlem1.k	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
72	71	fvmpt2 6983	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℚ ∧ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
73	67, 70, 72	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
74	73	ad4antlr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
75	66, 74	eleqtrrd 2864	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐾‘𝑝))
76		simp-5r 795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
77	76, 5	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ (𝐴 ∩ 𝐶))
78		ioogtlb 46035	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
79	37, 38, 39, 78	syl3anc 1389	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
80	79	ad5ant13 766	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐵 < 𝑝)
81	25	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
82	31	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
83		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
84		ioogtlb 46035	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
85	81, 82, 83, 84	syl3anc 1389	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
86	85	ad4ant14 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
87	77, 80, 86	jca32 523	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
88		rabid 3434	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
89	87, 88	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
90		rspe 3251	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ (𝐾‘𝑝) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
91	75, 89, 90	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
92	91	ex 416	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
93	92	ex 416	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑞 ∈ ℚ → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})))
94	45, 46, 93	rexlimd 3268	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
95	44, 94	mpd 15	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
96		eliun 4952	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
97	95, 96	sylibr 236	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
98	97	ex 416	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
99	98	reximdva 3174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
100	24, 99	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
101		eliun 4952	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
102	100, 101	sylibr 236	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
103	102	ex 416	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
104	96	rexbii 3108	. . . . . . . 8 ⊢ (∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
105	101, 104	bitri 277	. . . . . . 7 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
106	105	bilani 508	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
107	88	biimpi 218	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
108	107	simpld 498	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ (𝐴 ∩ 𝐶))
109	108	3ad2ant3 1147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ (𝐴 ∩ 𝐶))
110		elinel1 4153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐴)
111	110	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐴)
112	111, 8	syldan 600	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ ℝ)
113	108, 112	sylan2 602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 ∈ ℝ)
114	113	3adant2 1143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 ∈ ℝ)
115	108, 16	sylan2 602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 ∈ ℝ)
116	115	3adant2 1143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 ∈ ℝ)
117	114, 116	readdcld 11208	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) ∈ ℝ)
118		simp2l 1212	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℚ)
119	118, 28	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℝ)
120		ssrab2 4033	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ⊆ ℚ
121		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ (𝐾‘𝑝))
122	73	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
123	121, 122	eleqtrd 2863	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
124	120, 123	sselid 3934	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ ℚ)
125	124	3ad2ant2 1146	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℚ)
126	28	ssriv 3940	. . . . . . . . . . . . . . 15 ⊢ ℚ ⊆ ℝ
127	126	sseli 3932	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℝ)
128	125, 127	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℝ)
129	119, 128	readdcld 11208	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) ∈ ℝ)
130	11	3ad2ant1 1145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑅 ∈ ℝ)
131	107	simprld 781	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐵 < 𝑝)
132	131	3ad2ant3 1147	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 < 𝑝)
133	107	simprrd 783	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐷 < 𝑞)
134	133	3ad2ant3 1147	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 < 𝑞)
135	114, 116, 119, 128, 132, 134	ltadd12dd 45883	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < (𝑝 + 𝑞))
136		rabidim2 45644	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} → (𝑝 + 𝑞) < 𝑅)
137	123, 136	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑝 + 𝑞) < 𝑅)
138	137	3ad2ant2 1146	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) < 𝑅)
139	117, 129, 130, 135, 138	lttrd 11341	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < 𝑅)
140	109, 139	jca 519	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
141	140, 4	sylibr 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
142	141	3exp 1131	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})))
143	142	rexlimdvv 3217	. . . . . . 7 ⊢ (𝜑 → (∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
144	143	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
145	106, 144	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
146	145	ex 416	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
147	103, 146	impbid 214	. . 3 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
148	1, 147	alrimi 2247	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
149		nfrab1 3433	. . 3 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}
150		nfcv 2923	. . . 4 ⊢ Ⅎ𝑥ℚ
151		nfcv 2923	. . . . 5 ⊢ Ⅎ𝑥(𝐾‘𝑝)
152		nfrab1 3433	. . . . 5 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
153	151, 152	nfiun 4980	. . . 4 ⊢ Ⅎ𝑥∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
154	150, 153	nfiun 4980	. . 3 ⊢ Ⅎ𝑥∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
155	149, 154	cleqf 2951	. 2 ⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
156	148, 155	sylibr 236	1 ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 ∀wal 1557 = wceq 1559 Ⅎwnf 1802 ∈ wcel 2141 ∃wrex 3085 {crab 3413 Vcvv 3453 ∩ cin 3903 ∪ ciun 4948 class class class wbr 5099 ↦ cmpt 5180 ‘cfv 6517 (class class class)co 7392 ℝcr 11069 + caddc 11073 ℝ^*cxr 11212 < clt 11213 − cmin 11411 ℚcq 12946 (,)cioo 13346

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147 ax-pre-sup 11148

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-om 7843 df-1st 7966 df-2nd 7967 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-er 8673 df-en 8924 df-dom 8925 df-sdom 8926 df-sup 9385 df-inf 9386 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-n0 12479 df-z 12566 df-uz 12837 df-q 12947 df-ioo 13350

This theorem is referenced by: smfaddlem2 47302

W3C validator