Metamath Proof Explorer

Theorem 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 ⊢ Ⅎ 𝑥 𝜑
smfaddlem1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
smfaddlem1.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
smfaddlem1.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
smfaddlem1.k ⊢ 𝐾 = ( 𝑝 ∈ ℚ ↦ { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } )
Assertion smfaddlem1 ( 𝜑 → { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 + 𝐷 ) < 𝑅 } = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ ( 𝐾 ‘ 𝑝 ) { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 < 𝑝 ∧ 𝐷 < 𝑞 ) } )

Proof

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