Metamath Proof Explorer


Theorem icccmplem1

Description: Lemma for icccmp . (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses icccmp.1
|- J = ( topGen ` ran (,) )
icccmp.2
|- T = ( J |`t ( A [,] B ) )
icccmp.3
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
icccmp.4
|- S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }
icccmp.5
|- ( ph -> A e. RR )
icccmp.6
|- ( ph -> B e. RR )
icccmp.7
|- ( ph -> A <_ B )
icccmp.8
|- ( ph -> U C_ J )
icccmp.9
|- ( ph -> ( A [,] B ) C_ U. U )
Assertion icccmplem1
|- ( ph -> ( A e. S /\ A. y e. S y <_ B ) )

Proof

Step Hyp Ref Expression
1 icccmp.1
 |-  J = ( topGen ` ran (,) )
2 icccmp.2
 |-  T = ( J |`t ( A [,] B ) )
3 icccmp.3
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
4 icccmp.4
 |-  S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }
5 icccmp.5
 |-  ( ph -> A e. RR )
6 icccmp.6
 |-  ( ph -> B e. RR )
7 icccmp.7
 |-  ( ph -> A <_ B )
8 icccmp.8
 |-  ( ph -> U C_ J )
9 icccmp.9
 |-  ( ph -> ( A [,] B ) C_ U. U )
10 5 rexrd
 |-  ( ph -> A e. RR* )
11 6 rexrd
 |-  ( ph -> B e. RR* )
12 lbicc2
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
13 10 11 7 12 syl3anc
 |-  ( ph -> A e. ( A [,] B ) )
14 9 13 sseldd
 |-  ( ph -> A e. U. U )
15 eluni2
 |-  ( A e. U. U <-> E. u e. U A e. u )
16 14 15 sylib
 |-  ( ph -> E. u e. U A e. u )
17 snssi
 |-  ( u e. U -> { u } C_ U )
18 17 ad2antrl
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> { u } C_ U )
19 snex
 |-  { u } e. _V
20 19 elpw
 |-  ( { u } e. ~P U <-> { u } C_ U )
21 18 20 sylibr
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> { u } e. ~P U )
22 snfi
 |-  { u } e. Fin
23 22 a1i
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> { u } e. Fin )
24 21 23 elind
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> { u } e. ( ~P U i^i Fin ) )
25 10 adantr
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> A e. RR* )
26 iccid
 |-  ( A e. RR* -> ( A [,] A ) = { A } )
27 25 26 syl
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> ( A [,] A ) = { A } )
28 snssi
 |-  ( A e. u -> { A } C_ u )
29 28 ad2antll
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> { A } C_ u )
30 27 29 eqsstrd
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> ( A [,] A ) C_ u )
31 unieq
 |-  ( z = { u } -> U. z = U. { u } )
32 vex
 |-  u e. _V
33 32 unisn
 |-  U. { u } = u
34 31 33 eqtrdi
 |-  ( z = { u } -> U. z = u )
35 34 sseq2d
 |-  ( z = { u } -> ( ( A [,] A ) C_ U. z <-> ( A [,] A ) C_ u ) )
36 35 rspcev
 |-  ( ( { u } e. ( ~P U i^i Fin ) /\ ( A [,] A ) C_ u ) -> E. z e. ( ~P U i^i Fin ) ( A [,] A ) C_ U. z )
37 24 30 36 syl2anc
 |-  ( ( ph /\ ( u e. U /\ A e. u ) ) -> E. z e. ( ~P U i^i Fin ) ( A [,] A ) C_ U. z )
38 16 37 rexlimddv
 |-  ( ph -> E. z e. ( ~P U i^i Fin ) ( A [,] A ) C_ U. z )
39 oveq2
 |-  ( x = A -> ( A [,] x ) = ( A [,] A ) )
40 39 sseq1d
 |-  ( x = A -> ( ( A [,] x ) C_ U. z <-> ( A [,] A ) C_ U. z ) )
41 40 rexbidv
 |-  ( x = A -> ( E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z <-> E. z e. ( ~P U i^i Fin ) ( A [,] A ) C_ U. z ) )
42 41 4 elrab2
 |-  ( A e. S <-> ( A e. ( A [,] B ) /\ E. z e. ( ~P U i^i Fin ) ( A [,] A ) C_ U. z ) )
43 13 38 42 sylanbrc
 |-  ( ph -> A e. S )
44 4 ssrab3
 |-  S C_ ( A [,] B )
45 44 sseli
 |-  ( y e. S -> y e. ( A [,] B ) )
46 elicc2
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
47 5 6 46 syl2anc
 |-  ( ph -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
48 47 biimpa
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
49 48 simp3d
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y <_ B )
50 45 49 sylan2
 |-  ( ( ph /\ y e. S ) -> y <_ B )
51 50 ralrimiva
 |-  ( ph -> A. y e. S y <_ B )
52 43 51 jca
 |-  ( ph -> ( A e. S /\ A. y e. S y <_ B ) )