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 44994

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 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝜑)
3		inss1 4188	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ 𝐶) ⊆ 𝐴
4		rabid 3427	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
5	4	simplbi 498	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ (𝐴 ∩ 𝐶))
6	3, 5	sselid 3942	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ 𝐴)
7	6	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ 𝐴)
8		smfaddlem1.b	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	2, 7, 8	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ)
10	9	rexrd 11205	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ^*)
11		smfaddlem1.r	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℝ)
12	11	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑅 ∈ ℝ)
13		elinel2 4156	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐶)
14	13	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐶)
15		smfaddlem1.d	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)
16	14, 15	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐷 ∈ ℝ)
17	5, 16	sylan2 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐷 ∈ ℝ)
18	12, 17	resubcld 11583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ)
19	18	rexrd 11205	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ^*)
20	4	simprbi 497	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → (𝐵 + 𝐷) < 𝑅)
21	20	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝐵 + 𝐷) < 𝑅)
22	9, 17, 12	ltaddsubd 11755	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ((𝐵 + 𝐷) < 𝑅 ↔ 𝐵 < (𝑅 − 𝐷)))
23	21, 22	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 < (𝑅 − 𝐷))
24	10, 19, 23	qelioo 43774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
25	17	rexrd 11205	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐷 ∈ ℝ^*)
26	25	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 ∈ ℝ^*)
27	11	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑅 ∈ ℝ)
28		qre 12878	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℝ)
29	28	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℝ)
30	27, 29	resubcld 11583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ)
31	30	rexrd 11205	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ^*)
32	31	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑅 − 𝑝) ∈ ℝ^*)
33		elioore 13294	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → 𝑝 ∈ ℝ)
34	33	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 ∈ ℝ)
35	12	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑅 ∈ ℝ)
36	17	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 ∈ ℝ)
37	10	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 ∈ ℝ^*)
38	19	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑅 − 𝐷) ∈ ℝ^*)
39		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
40		iooltub 43738	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
41	37, 38, 39, 40	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
42	34, 35, 36, 41	ltsub13d 11761	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
43	42	adantlr 713	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
44	26, 32, 43	qelioo 43774	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
45		nfv 1917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞(((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
46		nfre1 3268	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
47		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℚ)
48		elioore 13294	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → 𝑞 ∈ ℝ)
49	48	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℝ)
50	35	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℝ)
51	33	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℝ)
52	50, 51	resubcld 11583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ)
53	25	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
54	52	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
55		simp3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
56		iooltub 43738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
57	53, 54, 55, 56	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
58	49, 52, 51, 57	ltadd2dd 11314	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < (𝑝 + (𝑅 − 𝑝)))
59	51	recnd 11183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℂ)
60	50	recnd 11183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℂ)
61	59, 60	pncan3d 11515	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + (𝑅 − 𝑝)) = 𝑅)
62	58, 61	breqtrd 5131	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
63	62	ad5ant135 1368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
64	47, 63	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
65		rabid 3427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ↔ (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
66	64, 65	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
67		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℚ)
68		qex 12886	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ ∈ V
69	68	rabex 5289	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V
70	69	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V)
71		smfaddlem1.k	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
72	71	fvmpt2 6959	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℚ ∧ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
73	67, 70, 72	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
74	73	ad4antlr 731	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
75	66, 74	eleqtrrd 2841	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐾‘𝑝))
76		simp-5r 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
77	76, 5	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ (𝐴 ∩ 𝐶))
78		ioogtlb 43723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
79	37, 38, 39, 78	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
80	79	ad5ant13 755	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐵 < 𝑝)
81	25	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
82	31	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
83		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
84		ioogtlb 43723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
85	81, 82, 83, 84	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
86	85	ad4ant14 750	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
87	77, 80, 86	jca32 516	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
88		rabid 3427	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
89	87, 88	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
90		rspe 3232	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ (𝐾‘𝑝) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
91	75, 89, 90	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
92	91	ex 413	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
93	92	ex 413	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑞 ∈ ℚ → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})))
94	45, 46, 93	rexlimd 3249	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
95	44, 94	mpd 15	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
96		eliun 4958	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
97	95, 96	sylibr 233	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
98	97	ex 413	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
99	98	reximdva 3165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
100	24, 99	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
101		eliun 4958	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
102	100, 101	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
103	102	ex 413	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
104	96	rexbii 3097	. . . . . . . . 9 ⊢ (∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
105	101, 104	bitri 274	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
106	105	biimpi 215	. . . . . . 7 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
107	106	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
108	88	biimpi 215	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
109	108	simpld 495	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ (𝐴 ∩ 𝐶))
110	109	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ (𝐴 ∩ 𝐶))
111		elinel1 4155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐴)
112	111	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐴)
113	112, 8	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ ℝ)
114	109, 113	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 ∈ ℝ)
115	114	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 ∈ ℝ)
116	109, 16	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 ∈ ℝ)
117	116	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 ∈ ℝ)
118	115, 117	readdcld 11184	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) ∈ ℝ)
119		simp2l 1199	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℚ)
120	119, 28	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℝ)
121		ssrab2 4037	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ⊆ ℚ
122		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ (𝐾‘𝑝))
123	73	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
124	122, 123	eleqtrd 2840	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
125	121, 124	sselid 3942	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ ℚ)
126	125	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℚ)
127	28	ssriv 3948	. . . . . . . . . . . . . . 15 ⊢ ℚ ⊆ ℝ
128	127	sseli 3940	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℝ)
129	126, 128	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℝ)
130	120, 129	readdcld 11184	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) ∈ ℝ)
131	11	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑅 ∈ ℝ)
132	108	simprld 770	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐵 < 𝑝)
133	132	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 < 𝑝)
134	108	simprrd 772	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐷 < 𝑞)
135	134	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 < 𝑞)
136	115, 117, 120, 129, 133, 135	ltadd12dd 43567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < (𝑝 + 𝑞))
137		rabidim2 43302	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} → (𝑝 + 𝑞) < 𝑅)
138	124, 137	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑝 + 𝑞) < 𝑅)
139	138	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) < 𝑅)
140	118, 130, 131, 136, 139	lttrd 11316	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < 𝑅)
141	110, 140	jca 512	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
142	141, 4	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
143	142	3exp 1119	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})))
144	143	rexlimdvv 3204	. . . . . . 7 ⊢ (𝜑 → (∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
145	144	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
146	107, 145	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
147	146	ex 413	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
148	103, 147	impbid 211	. . 3 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
149	1, 148	alrimi 2206	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
150		nfrab1 3426	. . 3 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}
151		nfcv 2907	. . . 4 ⊢ Ⅎ𝑥ℚ
152		nfcv 2907	. . . . 5 ⊢ Ⅎ𝑥(𝐾‘𝑝)
153		nfrab1 3426	. . . . 5 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
154	152, 153	nfiun 4984	. . . 4 ⊢ Ⅎ𝑥∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
155	151, 154	nfiun 4984	. . 3 ⊢ Ⅎ𝑥∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
156	150, 155	cleqf 2938	. 2 ⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
157	149, 156	sylibr 233	1 ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 ∀wal 1539 = wceq 1541 Ⅎwnf 1785 ∈ wcel 2106 ∃wrex 3073 {crab 3407 Vcvv 3445 ∩ cin 3909 ∪ ciun 4954 class class class wbr 5105 ↦ cmpt 5188 ‘cfv 6496 (class class class)co 7357 ℝcr 11050 + caddc 11054 ℝ^*cxr 11188 < clt 11189 − cmin 11385 ℚcq 12873 (,)cioo 13264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-sup 9378 df-inf 9379 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-n0 12414 df-z 12500 df-uz 12764 df-q 12874 df-ioo 13268

This theorem is referenced by: smfaddlem2 44995

W3C validator