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 
|- F/ x ph
smfaddlem1.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
smfaddlem1.d 
|- ( ( ph /\ x e. C ) -> D e. RR )
smfaddlem1.r 
|- ( ph -> R e. RR )
smfaddlem1.k 
|- K = ( p e. QQ |-> { q e. QQ | ( p + q ) < R } )
Assertion smfaddlem1 
|- ( ph -> { x e. ( A i^i C ) | ( B + D ) < R } = U_ p e. QQ U_ q e. ( K ` p ) { x e. ( A i^i C ) | ( B < p /\ D < q ) } )

Proof

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