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 46718

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 4244	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ 𝐶) ⊆ 𝐴
4		rabid 3454	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
5	4	simplbi 497	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ (𝐴 ∩ 𝐶))
6	3, 5	sselid 3992	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ 𝐴)
7	6	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ 𝐴)
8		smfaddlem1.b	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	2, 7, 8	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ)
10	9	rexrd 11308	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 ∈ ℝ^*)
11		smfaddlem1.r	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℝ)
12	11	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑅 ∈ ℝ)
13		elinel2 4211	. . . . . . . . . . . . 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 11688	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ)
19	18	rexrd 11308	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝑅 − 𝐷) ∈ ℝ^*)
20	4	simprbi 496	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → (𝐵 + 𝐷) < 𝑅)
21	20	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (𝐵 + 𝐷) < 𝑅)
22	9, 17, 12	ltaddsubd 11860	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ((𝐵 + 𝐷) < 𝑅 ↔ 𝐵 < (𝑅 − 𝐷)))
23	21, 22	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐵 < (𝑅 − 𝐷))
24	10, 19, 23	qelioo 45498	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
25	17	rexrd 11308	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝐷 ∈ ℝ^*)
26	25	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 ∈ ℝ^*)
27	11	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑅 ∈ ℝ)
28		qre 12992	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℝ)
29	28	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℝ)
30	27, 29	resubcld 11688	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ)
31	30	rexrd 11308	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑅 − 𝑝) ∈ ℝ^*)
32	31	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑅 − 𝑝) ∈ ℝ^*)
33		elioore 13413	. . . . . . . . . . . . . . 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 45462	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
41	37, 38, 39, 40	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑝 < (𝑅 − 𝐷))
42	34, 35, 36, 41	ltsub13d 11866	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
43	42	adantlr 715	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐷 < (𝑅 − 𝑝))
44	26, 32, 43	qelioo 45498	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
45		nfv 1911	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞(((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)))
46		nfre1 3282	. . . . . . . . . . . 12 ⊢ Ⅎ𝑞∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
47		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℚ)
48		elioore 13413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → 𝑞 ∈ ℝ)
49	48	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ ℝ)
50	35	3adant3 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℝ)
51	33	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℝ)
52	50, 51	resubcld 11688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ)
53	25	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
54	52	rexrd 11308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
55		simp3 1137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
56		iooltub 45462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
57	53, 54, 55, 56	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 < (𝑅 − 𝑝))
58	49, 52, 51, 57	ltadd2dd 11417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < (𝑝 + (𝑅 − 𝑝)))
59	51	recnd 11286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑝 ∈ ℂ)
60	50	recnd 11286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑅 ∈ ℂ)
61	59, 60	pncan3d 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + (𝑅 − 𝑝)) = 𝑅)
62	58, 61	breqtrd 5173	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
63	62	ad5ant135 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑝 + 𝑞) < 𝑅)
64	47, 63	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
65		rabid 3454	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ↔ (𝑞 ∈ ℚ ∧ (𝑝 + 𝑞) < 𝑅))
66	64, 65	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
67		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℚ)
68		qex 13000	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ ∈ V
69	68	rabex 5344	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V
70	69	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V)
71		smfaddlem1.k	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
72	71	fvmpt2 7026	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℚ ∧ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ∈ V) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
73	67, 70, 72	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
74	73	ad4antlr 733	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
75	66, 74	eleqtrrd 2841	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐾‘𝑝))
76		simp-5r 786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
77	76, 5	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ (𝐴 ∩ 𝐶))
78		ioogtlb 45447	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑅 − 𝐷) ∈ ℝ^* ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
79	37, 38, 39, 78	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝐵 < 𝑝)
80	79	ad5ant13 757	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐵 < 𝑝)
81	25	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 ∈ ℝ^*)
82	31	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑅 − 𝑝) ∈ ℝ^*)
83		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)))
84		ioogtlb 45447	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℝ^* ∧ (𝑅 − 𝑝) ∈ ℝ^* ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
85	81, 82, 83, 84	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
86	85	ad4ant14 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝐷 < 𝑞)
87	77, 80, 86	jca32 515	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
88		rabid 3454	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)))
89	87, 88	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
90		rspe 3246	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ (𝐾‘𝑝) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
91	75, 89, 90	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) ∧ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
92	91	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) ∧ 𝑞 ∈ ℚ) → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
93	92	ex 412	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (𝑞 ∈ ℚ → (𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})))
94	45, 46, 93	rexlimd 3263	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → (∃𝑞 ∈ ℚ 𝑞 ∈ (𝐷(,)(𝑅 − 𝑝)) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
95	44, 94	mpd 15	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
96		eliun 4999	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑞 ∈ (𝐾‘𝑝)𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
97	95, 96	sylibr 234	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) ∧ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷))) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
98	97	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) ∧ 𝑝 ∈ ℚ) → (𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
99	98	reximdva 3165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → (∃𝑝 ∈ ℚ 𝑝 ∈ (𝐵(,)(𝑅 − 𝐷)) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
100	24, 99	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
101		eliun 4999	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∃𝑝 ∈ ℚ 𝑥 ∈ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
102	100, 101	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}) → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
103	102	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} → 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
104	96	rexbii 3091	. . . . . . . . 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 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ (𝐴 ∩ 𝐶))
111		elinel1 4210	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐴)
112	111	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐴)
113	112, 8	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ ℝ)
114	109, 113	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 ∈ ℝ)
115	114	3adant2 1130	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 ∈ ℝ)
116	109, 16	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 ∈ ℝ)
117	116	3adant2 1130	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 ∈ ℝ)
118	115, 117	readdcld 11287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) ∈ ℝ)
119		simp2l 1198	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℚ)
120	119, 28	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑝 ∈ ℝ)
121		ssrab2 4089	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} ⊆ ℚ
122		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ (𝐾‘𝑝))
123	73	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝐾‘𝑝) = {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
124	122, 123	eleqtrd 2840	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})
125	121, 124	sselid 3992	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → 𝑞 ∈ ℚ)
126	125	3ad2ant2 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℚ)
127	28	ssriv 3998	. . . . . . . . . . . . . . 15 ⊢ ℚ ⊆ ℝ
128	127	sseli 3990	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℝ)
129	126, 128	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑞 ∈ ℝ)
130	120, 129	readdcld 11287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) ∈ ℝ)
131	11	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑅 ∈ ℝ)
132	108	simprld 772	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐵 < 𝑝)
133	132	3ad2ant3 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐵 < 𝑝)
134	108	simprrd 774	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝐷 < 𝑞)
135	134	3ad2ant3 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝐷 < 𝑞)
136	115, 117, 120, 129, 133, 135	ltadd12dd 45292	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < (𝑝 + 𝑞))
137		rabidim2 45041	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅} → (𝑝 + 𝑞) < 𝑅)
138	124, 137	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑝 + 𝑞) < 𝑅)
139	138	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑝 + 𝑞) < 𝑅)
140	118, 130, 131, 136, 139	lttrd 11419	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝐵 + 𝐷) < 𝑅)
141	110, 140	jca 511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 + 𝐷) < 𝑅))
142	141, 4	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) ∧ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})
143	142	3exp 1118	. . . . . . . 8 ⊢ (𝜑 → ((𝑝 ∈ ℚ ∧ 𝑞 ∈ (𝐾‘𝑝)) → (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅})))
144	143	rexlimdvv 3209	. . . . . . 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 2210	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
150		nfrab1 3453	. . 3 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅}
151		nfcv 2902	. . . 4 ⊢ Ⅎ𝑥ℚ
152		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑥(𝐾‘𝑝)
153		nfrab1 3453	. . . . 5 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
154	152, 153	nfiun 5027	. . . 4 ⊢ Ⅎ𝑥∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
155	151, 154	nfiun 5027	. . 3 ⊢ Ⅎ𝑥∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}
156	150, 155	cleqf 2931	. 2 ⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)} ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ↔ 𝑥 ∈ ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)}))
157	149, 156	sylibr 234	1 ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1534 = wceq 1536 Ⅎwnf 1779 ∈ wcel 2105 ∃wrex 3067 {crab 3432 Vcvv 3477 ∩ cin 3961 ∪ ciun 4995 class class class wbr 5147 ↦ cmpt 5230 ‘cfv 6562 (class class class)co 7430 ℝcr 11151 + caddc 11155 ℝ^*cxr 11291 < clt 11292 − cmin 11489 ℚcq 12987 (,)cioo 13383

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229 ax-pre-sup 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-er 8743 df-en 8984 df-dom 8985 df-sdom 8986 df-sup 9479 df-inf 9480 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-div 11918 df-nn 12264 df-n0 12524 df-z 12611 df-uz 12876 df-q 12988 df-ioo 13387

This theorem is referenced by: smfaddlem2 46719

W3C validator