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 ) )