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 46885

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 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝜑)
3		inss1 4186	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ 𝐶) ⊆ 𝐴
4		rabid 3417	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
5	4	simplbi 497	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ (𝐴 ∩ 𝐶))
6	3, 5	sselid 3928	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ 𝐴)
7	6	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ 𝐴)
8		smfaddlem1.b	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	2, 7, 8	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ)
10	9	rexrd 11169	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ^*)
11		smfaddlem1.r	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℝ)
12	11	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑅 ∈ ℝ)
13		elinel2 4151	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐶)
14	13	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐶)
15		smfaddlem1.d	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)
16	14, 15	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐷 ∈ ℝ)
17	5, 16	sylan2 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐷 ∈ ℝ)
18	12, 17	resubcld 11552	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ)
19	18	rexrd 11169	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ^*)
20	4	simprbi 496	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → (𝐵 + 𝐷) < 𝑅)
21	20	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝐵 + 𝐷) < 𝑅)
22	9, 17, 12	ltaddsubd 11724	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ((𝐵 + 𝐷) < 𝑅 ↔ 𝐵 < (𝑅 − 𝐷)))
23	21, 22	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 < (𝑅 − 𝐷))
24	10, 19, 23	qelioo 45670	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
25	17	rexrd 11169	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐷 ∈ ℝ^*)
26	25	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 ∈ ℝ^*)
27	11	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑅 ∈ ℝ)
28		qre 12853	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℝ)
29	28	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℝ)
30	27, 29	resubcld 11552	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ)
31	30	rexrd 11169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ^*)
32	31	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑅 − 𝑝) ∈ ℝ^*)
33		elioore 13277	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → 𝑝 ∈ ℝ)
34	33	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 ∈ ℝ)
35	12	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑅 ∈ ℝ)
36	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 ∈ ℝ)
37	10	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 ∈ ℝ^*)
38	19	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑅 − 𝐷) ∈ ℝ^*)
39		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
40		iooltub 45634	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
41	37, 38, 39, 40	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
42	34, 35, 36, 41	ltsub13d 11730	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
43	42	adantlr 715	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
44	26, 32, 43	qelioo 45670	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
45		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞(((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
46		nfre1 3258	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
47		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℚ)
48		elioore 13277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → 𝑞 ∈ ℝ)
49	48	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℝ)
50	35	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℝ)
51	33	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℝ)
52	50, 51	resubcld 11552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ)
53	25	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
54	52	rexrd 11169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
55		simp3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
56		iooltub 45634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
57	53, 54, 55, 56	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
58	49, 52, 51, 57	ltadd2dd 11279	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < (𝑝 + (𝑅 − 𝑝)))
59	51	recnd 11147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℂ)
60	50	recnd 11147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℂ)
61	59, 60	pncan3d 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + (𝑅 − 𝑝)) = 𝑅)
62	58, 61	breqtrd 5119	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
63	62	ad5ant135 1370	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
64	47, 63	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
65		rabid 3417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ↔ (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
66	64, 65	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
67		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℚ)
68		qex 12861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ ∈ V
69	68	rabex 5279	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V
70	69	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V)
71		smfaddlem1.k	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
72	71	fvmpt2 6946	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℚ ∧ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
73	67, 70, 72	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
74	73	ad4antlr 733	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
75	66, 74	eleqtrrd 2836	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐾‘𝑝))
76		simp-5r 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
77	76, 5	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ (𝐴 ∩ 𝐶))
78		ioogtlb 45619	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
79	37, 38, 39, 78	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
80	79	ad5ant13 756	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐵 < 𝑝)
81	25	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
82	31	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
83		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
84		ioogtlb 45619	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
85	81, 82, 83, 84	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
86	85	ad4ant14 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
87	77, 80, 86	jca32 515	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
88		rabid 3417	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
89	87, 88	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
90		rspe 3223	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ (𝐾‘𝑝) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
91	75, 89, 90	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
92	91	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
93	92	ex 412	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑞 ∈ ℚ → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})))
94	45, 46, 93	rexlimd 3240	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
95	44, 94	mpd 15	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
96		eliun 4945	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
97	95, 96	sylibr 234	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
98	97	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
99	98	reximdva 3146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
100	24, 99	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
101		eliun 4945	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
102	100, 101	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
103	102	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
104	96	rexbii 3080	. . . . . . . . 9 ⊢ (∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
105	101, 104	bitri 275	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
106	105	biimpi 216	. . . . . . 7 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
107	106	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → ∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
108	88	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
109	108	simpld 494	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ (𝐴 ∩ 𝐶))
110	109	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ (𝐴 ∩ 𝐶))
111		elinel1 4150	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐴)
112	111	adantl 481	. . . . . . . . . . . . . . . 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 11148	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) ∈ ℝ)
119		simp2l 1200	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℚ)
120	119, 28	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℝ)
121		ssrab2 4029	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ⊆ ℚ
122		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ (𝐾‘𝑝))
123	73	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
124	122, 123	eleqtrd 2835	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
125	121, 124	sselid 3928	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ ℚ)
126	125	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℚ)
127	28	ssriv 3934	. . . . . . . . . . . . . . 15 ⊢ ℚ ⊆ ℝ
128	127	sseli 3926	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℝ)
129	126, 128	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℝ)
130	120, 129	readdcld 11148	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) ∈ ℝ)
131	11	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑅 ∈ ℝ)
132	108	simprld 771	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐵 < 𝑝)
133	132	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 < 𝑝)
134	108	simprrd 773	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐷 < 𝑞)
135	134	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 < 𝑞)
136	115, 117, 120, 129, 133, 135	ltadd12dd 45466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < (𝑝 + 𝑞))
137		rabidim2 45223	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} → (𝑝 + 𝑞) < 𝑅)
138	124, 137	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑝 + 𝑞) < 𝑅)
139	138	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) < 𝑅)
140	118, 130, 131, 136, 139	lttrd 11281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < 𝑅)
141	110, 140	jca 511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
142	141, 4	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
143	142	3exp 1119	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})))
144	143	rexlimdvv 3189	. . . . . . 7 ⊢ (𝜑 → (∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
145	144	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (∃𝑝 ∈ ℚ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
146	107, 145	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
147	146	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}))
148	103, 147	impbid 212	. . 3 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
149	1, 148	alrimi 2218	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
150		nfrab1 3416	. . 3 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}
151		nfcv 2895	. . . 4 ⊢ Ⅎ𝑥ℚ
152		nfcv 2895	. . . . 5 ⊢ Ⅎ𝑥(𝐾‘𝑝)
153		nfrab1 3416	. . . . 5 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
154	152, 153	nfiun 4973	. . . 4 ⊢ Ⅎ𝑥∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
155	151, 154	nfiun 4973	. . 3 ⊢ Ⅎ𝑥∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
156	150, 155	cleqf 2924	. 2 ⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
157	149, 156	sylibr 234	1 ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1539 = wceq 1541 Ⅎwnf 1784 ∈ wcel 2113 ∃wrex 3057 {crab 3396 Vcvv 3437 ∩ cin 3897 ∪ ciun 4941 class class class wbr 5093 ↦ cmpt 5174 ‘cfv 6486 (class class class)co 7352 ℝcr 11012 + caddc 11016 ℝ^*cxr 11152 < clt 11153 − cmin 11351 ℚcq 12848 (,)cioo 13247

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090 ax-pre-sup 11091

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-sup 9333 df-inf 9334 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-div 11782 df-nn 12133 df-n0 12389 df-z 12476 df-uz 12739 df-q 12849 df-ioo 13251

This theorem is referenced by: smfaddlem2 46886

W3C validator