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	biimpi	$⊢ 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	106	adantl	$⊢ (φ \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)\}$
108	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))$
109	108	simpld	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to x \in (A \cap C)$
110	109	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)$
111		elinel1	$⊢ x \in (A \cap C) \to x \in A$
112	111	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in A$
113	112 2	syldan	$⊢ (φ \land x \in (A \cap C)) \to B \in ℝ$
114	109 113	sylan2	$⊢ (φ \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to B \in ℝ$
115	114	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 ℝ$
116	109 17	sylan2	$⊢ (φ \land x \in \{x \in (A \cap C) \| (B < p \land D < q)\}) \to D \in ℝ$
117	116	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 ℝ$
118	115 117	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 ℝ$
119		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 ℚ$
120	119 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 ℝ$
121		ssrab2	$⊢ \{q \in ℚ \| p + q < R\} \subseteq ℚ$
122		simpr	$⊢ (p \in ℚ \land q \in K (p)) \to q \in K (p)$
123	73	adantr	$⊢ (p \in ℚ \land q \in K (p)) \to K (p) = \{q \in ℚ \| p + q < R\}$
124	122 123	eleqtrd	$⊢ (p \in ℚ \land q \in K (p)) \to q \in \{q \in ℚ \| p + q < R\}$
125	121 124	sselid	$⊢ (p \in ℚ \land q \in K (p)) \to q \in ℚ$
126	125	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 ℚ$
127	29	ssriv	$⊢ ℚ \subseteq ℝ$
128	127	sseli	$⊢ q \in ℚ \to q \in ℝ$
129	126 128	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 ℝ$
130	120 129	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 ℝ$
131	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 ℝ$
132	108	simprld	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to B < p$
133	132	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$
134	108	simprrd	$⊢ x \in \{x \in (A \cap C) \| (B < p \land D < q)\} \to D < q$
135	134	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$
136	115 117 120 129 133 135	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$
137		rabidim2	$⊢ q \in \{q \in ℚ \| p + q < R\} \to p + q < R$
138	124 137	syl	$⊢ (p \in ℚ \land q \in K (p)) \to p + q < R$
139	138	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$
140	118 130 131 136 139	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$
141	110 140	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)$
142	141 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\}$
143	142	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\}))$
144	143	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\})$
145	144	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\})$
146	107 145	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\}$
147	146	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\})$
148	103 147	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)\})$
149	1 148	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)\})$
150		nfrab1	$⊢ \underline{Ⅎ} x \{x \in (A \cap C) \| B + D < R\}$
151		nfcv	$⊢ \underline{Ⅎ} x ℚ$
152		nfcv	$⊢ \underline{Ⅎ} x K (p)$
153		nfrab1	$⊢ \underline{Ⅎ} x \{x \in (A \cap C) \| (B < p \land D < q)\}$
154	152 153	nfiun	$⊢ \underline{Ⅎ} x ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
155	151 154	nfiun	$⊢ \underline{Ⅎ} x ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
156	150 155	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)\})$
157	149 156	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