smfaddlem1

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)

	Ref	Expression
Hypotheses	smfaddlem1.x	$⊢ Ⅎ x φ$
	smfaddlem1.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	smfaddlem1.d	$⊢ (φ \land x \in C) \to D \in ℝ$
	smfaddlem1.r	$⊢ φ \to R \in ℝ$
	smfaddlem1.k	$⊢ K = (p \in ℚ ⟼ \{q \in ℚ \| p + q < R\})$
Assertion	smfaddlem1	$⊢ φ \to \{x \in (A \cap C) \| B + D < R\} = ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$

Proof

Step	Hyp	Ref	Expression
1		smfaddlem1.x	$⊢ Ⅎ x φ$
2		smfaddlem1.b	$⊢ (φ \land x \in A) \to B \in ℝ$
3		smfaddlem1.d	$⊢ (φ \land x \in C) \to D \in ℝ$
4		smfaddlem1.r	$⊢ φ \to R \in ℝ$
5		smfaddlem1.k	$⊢ K = (p \in ℚ ⟼ \{q \in ℚ \| p + q < R\})$
6		simpl	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to φ$
7		inss1	$⊢ A \cap C \subseteq A$
8		rabid	$⊢ x \in \{x \in (A \cap C) \| B + D < R\} \leftrightarrow (x \in (A \cap C) \land B + D < R)$
9	8	simplbi	$⊢ x \in \{x \in (A \cap C) \| B + D < R\} \to x \in (A \cap C)$
10	7 9	sselid	$⊢ x \in \{x \in (A \cap C) \| B + D < R\} \to x \in A$
11	10	adantl	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to x \in A$
12	6 11 2	syl2anc	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to B \in ℝ$
13	12	rexrd	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to B \in ℝ^{*}$
14	4	adantr	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to R \in ℝ$
15		elinel2	$⊢ x \in (A \cap C) \to x \in C$
16	15	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in C$
17	16 3	syldan	$⊢ (φ \land x \in (A \cap C)) \to D \in ℝ$
18	9 17	sylan2	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to D \in ℝ$
19	14 18	resubcld	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to R - D \in ℝ$
20	19	rexrd	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to R - D \in ℝ^{*}$
21	8	simprbi	$⊢ x \in \{x \in (A \cap C) \| B + D < R\} \to B + D < R$
22	21	adantl	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to B + D < R$
23	12 18 14	ltaddsubd	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to (B + D < R \leftrightarrow B < R - D)$
24	22 23	mpbid	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to B < R - D$
25	13 20 24	qelioo	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to \exists p \in ℚ p \in (B, R - D)$
26	18	rexrd	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to D \in ℝ^{*}$
27	26	ad2antrr	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to D \in ℝ^{*}$
28	4	ad2antrr	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \to R \in ℝ$
29		qre	$⊢ p \in ℚ \to p \in ℝ$
30	29	adantl	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \to p \in ℝ$
31	28 30	resubcld	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \to R - p \in ℝ$
32	31	rexrd	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \to R - p \in ℝ^{*}$
33	32	adantr	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to R - p \in ℝ^{*}$
34		elioore	$⊢ p \in (B, R - D) \to p \in ℝ$
35	34	adantl	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to p \in ℝ$
36	14	adantr	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to R \in ℝ$
37	18	adantr	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to D \in ℝ$
38	13	adantr	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to B \in ℝ^{*}$
39	20	adantr	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to R - D \in ℝ^{*}$
40		simpr	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to p \in (B, R - D)$
41		iooltub	$⊢ (B \in ℝ^{} \land R - D \in ℝ^{} \land p \in (B, R - D)) \to p < R - D$
42	38 39 40 41	syl3anc	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to p < R - D$
43	35 36 37 42	ltsub13d	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to D < R - p$
44	43	adantlr	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to D < R - p$
45	27 33 44	qelioo	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to \exists q \in ℚ q \in (D, R - p)$
46		nfv	$⊢ Ⅎ q (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D))$
47		nfre1	$⊢ Ⅎ q \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
48		simplr	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to q \in ℚ$
49		elioore	$⊢ q \in (D, R - p) \to q \in ℝ$
50	49	3ad2ant3	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to q \in ℝ$
51	36	3adant3	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to R \in ℝ$
52	34	3ad2ant2	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to p \in ℝ$
53	51 52	resubcld	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to R - p \in ℝ$
54	26	3ad2ant1	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to D \in ℝ^{*}$
55	53	rexrd	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to R - p \in ℝ^{*}$
56		simp3	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to q \in (D, R - p)$
57		iooltub	$⊢ (D \in ℝ^{} \land R - p \in ℝ^{} \land q \in (D, R - p)) \to q < R - p$
58	54 55 56 57	syl3anc	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to q < R - p$
59	50 53 52 58	ltadd2dd	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to p + q < p + R - p$
60	52	recnd	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to p \in ℂ$
61	51	recnd	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to R \in ℂ$
62	60 61	pncan3d	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to p + R - p = R$
63	59 62	breqtrd	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D) \land q \in (D, R - p)) \to p + q < R$
64	63	ad5ant135	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to p + q < R$
65	48 64	jca	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to (q \in ℚ \land p + q < R)$
66		rabid	$⊢ q \in \{q \in ℚ \| p + q < R\} \leftrightarrow (q \in ℚ \land p + q < R)$
67	65 66	sylibr	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to q \in \{q \in ℚ \| p + q < R\}$
68		id	$⊢ p \in ℚ \to p \in ℚ$
69		qex	$⊢ ℚ \in V$
70	69	rabex	$⊢ \{q \in ℚ \| p + q < R\} \in V$
71	70	a1i	$⊢ p \in ℚ \to \{q \in ℚ \| p + q < R\} \in V$
72	5	fvmpt2	$⊢ (p \in ℚ \land \{q \in ℚ \| p + q < R\} \in V) \to K (p) = \{q \in ℚ \| p + q < R\}$
73	68 71 72	syl2anc	$⊢ p \in ℚ \to K (p) = \{q \in ℚ \| p + q < R\}$
74	73	ad4antlr	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to K (p) = \{q \in ℚ \| p + q < R\}$
75	67 74	eleqtrrd	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to q \in K (p)$
76		simp-5r	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to x \in \{x \in (A \cap C) \| B + D < R\}$
77	76 9	syl	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to x \in (A \cap C)$
78		ioogtlb	$⊢ (B \in ℝ^{} \land R - D \in ℝ^{} \land p \in (B, R - D)) \to B < p$
79	38 39 40 78	syl3anc	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in (B, R - D)) \to B < p$
80	79	ad5ant13	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to B < p$
81	26	ad2antrr	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land q \in (D, R - p)) \to D \in ℝ^{*}$
82	32	adantr	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land q \in (D, R - p)) \to R - p \in ℝ^{*}$
83		simpr	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land q \in (D, R - p)) \to q \in (D, R - p)$
84		ioogtlb	$⊢ (D \in ℝ^{} \land R - p \in ℝ^{} \land q \in (D, R - p)) \to D < q$
85	81 82 83 84	syl3anc	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land q \in (D, R - p)) \to D < q$
86	85	ad4ant14	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to D < q$
87	77 80 86	jca32	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to (x \in (A \cap C) \land (B < p \land D < q))$
88		rabid	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \leftrightarrow (x \in (A \cap C) \land (B < p \land D < q))$
89	87 88	sylibr	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
90		rspe	$⊢ (q \in K (p) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
91	75 89 90	syl2anc	$⊢ (((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \land q \in (D, R - p)) \to \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
92	91	ex	$⊢ ((((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \land q \in ℚ) \to (q \in (D, R - p) \to \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\})$
93	92	ex	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to (q \in ℚ \to (q \in (D, R - p) \to \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}))$
94	46 47 93	rexlimd	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to (\exists q \in ℚ q \in (D, R - p) \to \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\})$
95	45 94	mpd	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
96		eliun	$⊢ x \in ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \leftrightarrow \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
97	95 96	sylibr	$⊢ (((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \land p \in (B, R - D)) \to x \in ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
98	97	ex	$⊢ ((φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \land p \in ℚ) \to (p \in (B, R - D) \to x \in ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\})$
99	98	reximdva	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to (\exists p \in ℚ p \in (B, R - D) \to \exists p \in ℚ x \in ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\})$
100	25 99	mpd	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to \exists p \in ℚ x \in ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
101		eliun	$⊢ x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \leftrightarrow \exists p \in ℚ x \in ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
102	100 101	sylibr	$⊢ (φ \land x \in \{x \in (A \cap C) \| B + D < R\}) \to x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
103	102	ex	$⊢ φ \to (x \in \{x \in (A \cap C) \| B + D < R\} \to x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\})$
104	96	rexbii	$⊢ \exists p \in ℚ x \in ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \leftrightarrow \exists p \in ℚ \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
105	101 104	bitri	$⊢ x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \leftrightarrow \exists p \in ℚ \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
106	105	bilani	$⊢ (φ \land x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}) \to \exists p \in ℚ \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\}$
107	88	biimpi	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to (x \in (A \cap C) \land (B < p \land D < q))$
108	107	simpld	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to x \in (A \cap C)$
109	108	3ad2ant3	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to x \in (A \cap C)$
110		elinel1	$⊢ x \in (A \cap C) \to x \in A$
111	110	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in A$
112	111 2	syldan	$⊢ (φ \land x \in (A \cap C)) \to B \in ℝ$
113	108 112	sylan2	$⊢ (φ \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to B \in ℝ$
114	113	3adant2	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to B \in ℝ$
115	108 17	sylan2	$⊢ (φ \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to D \in ℝ$
116	115	3adant2	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to D \in ℝ$
117	114 116	readdcld	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to B + D \in ℝ$
118		simp2l	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to p \in ℚ$
119	118 29	syl	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to p \in ℝ$
120		ssrab2	$⊢ \{q \in ℚ \| p + q < R\} \subseteq ℚ$
121		simpr	$⊢ (p \in ℚ \land q \in K (p)) \to q \in K (p)$
122	73	adantr	$⊢ (p \in ℚ \land q \in K (p)) \to K (p) = \{q \in ℚ \| p + q < R\}$
123	121 122	eleqtrd	$⊢ (p \in ℚ \land q \in K (p)) \to q \in \{q \in ℚ \| p + q < R\}$
124	120 123	sselid	$⊢ (p \in ℚ \land q \in K (p)) \to q \in ℚ$
125	124	3ad2ant2	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to q \in ℚ$
126	29	ssriv	$⊢ ℚ \subseteq ℝ$
127	126	sseli	$⊢ q \in ℚ \to q \in ℝ$
128	125 127	syl	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to q \in ℝ$
129	119 128	readdcld	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to p + q \in ℝ$
130	4	3ad2ant1	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to R \in ℝ$
131	107	simprld	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to B < p$
132	131	3ad2ant3	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to B < p$
133	107	simprrd	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to D < q$
134	133	3ad2ant3	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to D < q$
135	114 116 119 128 132 134	ltadd12dd	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to B + D < p + q$
136		rabidim2	$⊢ q \in \{q \in ℚ \| p + q < R\} \to p + q < R$
137	123 136	syl	$⊢ (p \in ℚ \land q \in K (p)) \to p + q < R$
138	137	3ad2ant2	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to p + q < R$
139	117 129 130 135 138	lttrd	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to B + D < R$
140	109 139	jca	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to (x \in (A \cap C) \land B + D < R)$
141	140 8	sylibr	$⊢ (φ \land (p \in ℚ \land q \in K (p)) \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to x \in \{x \in (A \cap C) \| B + D < R\}$
142	141	3exp	$⊢ φ \to ((p \in ℚ \land q \in K (p)) \to (x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to x \in \{x \in (A \cap C) \| B + D < R\}))$
143	142	rexlimdvv	$⊢ φ \to (\exists p \in ℚ \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to x \in \{x \in (A \cap C) \| B + D < R\})$
144	143	adantr	$⊢ (φ \land x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}) \to (\exists p \in ℚ \exists q \in K (p) x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to x \in \{x \in (A \cap C) \| B + D < R\})$
145	106 144	mpd	$⊢ (φ \land x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}) \to x \in \{x \in (A \cap C) \| B + D < R\}$
146	145	ex	$⊢ φ \to (x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \to x \in \{x \in (A \cap C) \| B + D < R\})$
147	103 146	impbid	$⊢ φ \to (x \in \{x \in (A \cap C) \| B + D < R\} \leftrightarrow x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\})$
148	1 147	alrimi	$⊢ φ \to \forall x (x \in \{x \in (A \cap C) \| B + D < R\} \leftrightarrow x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\})$
149		nfrab1	$⊢ \underline{Ⅎ} x \{x \in (A \cap C) \| B + D < R\}$
150		nfcv	$⊢ \underline{Ⅎ} x ℚ$
151		nfcv	$⊢ \underline{Ⅎ} x K (p)$
152		nfrab1	$⊢ \underline{Ⅎ} x \{x \in (A \cap C) \| (B < p \land D < q)\}$
153	151 152	nfiun	$⊢ \underline{Ⅎ} x ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
154	150 153	nfiun	$⊢ \underline{Ⅎ} x ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
155	149 154	cleqf	$⊢ \{x \in (A \cap C) \| B + D < R\} = ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \leftrightarrow \forall x (x \in \{x \in (A \cap C) \| B + D < R\} \leftrightarrow x \in ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\})$
156	148 155	sylibr	$⊢ φ \to \{x \in (A \cap C) \| B + D < R\} = ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$

Metamath Proof Explorer

Theorem smfaddlem1

Proof