Metamath Proof Explorer

Theorem dedekindle

Description: The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013)

Ref Expression
Assertion dedekindle 
|- ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )

Proof

Step Hyp Ref Expression
1 simpr1 
 |-  ( ( ( A i^i B ) = (/) /\ ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) ) -> A C_ RR )
2 simpr2 
 |-  ( ( ( A i^i B ) = (/) /\ ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) ) -> B C_ RR )
3 simp1 
 |-  ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) -> ( A i^i B ) = (/) )
4 simpl 
 |-  ( ( x e. A /\ y e. B ) -> x e. A )
5 disjel 
 |-  ( ( ( A i^i B ) = (/) /\ x e. A ) -> -. x e. B )
6 3 4 5 syl2an 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> -. x e. B )
7 eleq1w 
 |-  ( y = x -> ( y e. B <-> x e. B ) )
8 7 biimpcd 
 |-  ( y e. B -> ( y = x -> x e. B ) )
9 8 necon3bd 
 |-  ( y e. B -> ( -. x e. B -> y =/= x ) )
10 9 ad2antll 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> ( -. x e. B -> y =/= x ) )
11 6 10 mpd 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> y =/= x )
12 simp2 
 |-  ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) -> A C_ RR )
13 ssel2 
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
14 12 4 13 syl2an 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> x e. RR )
15 simp3 
 |-  ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) -> B C_ RR )
16 simpr 
 |-  ( ( x e. A /\ y e. B ) -> y e. B )
17 ssel2 
 |-  ( ( B C_ RR /\ y e. B ) -> y e. RR )
18 15 16 17 syl2an 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> y e. RR )
19 14 18 ltlend 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> ( x < y <-> ( x <_ y /\ y =/= x ) ) )
20 19 biimprd 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> ( ( x <_ y /\ y =/= x ) -> x < y ) )
21 11 20 mpan2d 
 |-  ( ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) /\ ( x e. A /\ y e. B ) ) -> ( x <_ y -> x < y ) )
22 21 ralimdvva 
 |-  ( ( ( A i^i B ) = (/) /\ A C_ RR /\ B C_ RR ) -> ( A. x e. A A. y e. B x <_ y -> A. x e. A A. y e. B x < y ) )
23 22 3exp 
 |-  ( ( A i^i B ) = (/) -> ( A C_ RR -> ( B C_ RR -> ( A. x e. A A. y e. B x <_ y -> A. x e. A A. y e. B x < y ) ) ) )
24 23 3imp2 
 |-  ( ( ( A i^i B ) = (/) /\ ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) ) -> A. x e. A A. y e. B x < y )
25 dedekind 
 |-  ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
26 1 2 24 25 syl3anc 
 |-  ( ( ( A i^i B ) = (/) /\ ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
27 26 ex 
 |-  ( ( A i^i B ) = (/) -> ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) )
28 n0 
 |-  ( ( A i^i B ) =/= (/) <-> E. w w e. ( A i^i B ) )
29 simp1 
 |-  ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> A C_ RR )
30 elinel1 
 |-  ( w e. ( A i^i B ) -> w e. A )
31 ssel2 
 |-  ( ( A C_ RR /\ w e. A ) -> w e. RR )
32 29 30 31 syl2an 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ w e. ( A i^i B ) ) -> w e. RR )
33 nfv 
 |-  F/ x A C_ RR
34 nfv 
 |-  F/ x B C_ RR
35 nfra1 
 |-  F/ x A. x e. A A. y e. B x <_ y
36 33 34 35 nf3an 
 |-  F/ x ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y )
37 nfv 
 |-  F/ x w e. ( A i^i B )
38 36 37 nfan 
 |-  F/ x ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ w e. ( A i^i B ) )
39 nfv 
 |-  F/ y A C_ RR
40 nfv 
 |-  F/ y B C_ RR
41 nfra2w 
 |-  F/ y A. x e. A A. y e. B x <_ y
42 39 40 41 nf3an 
 |-  F/ y ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y )
43 nfv 
 |-  F/ y ( w e. ( A i^i B ) /\ x e. A )
44 42 43 nfan 
 |-  F/ y ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) )
45 rsp 
 |-  ( A. x e. A A. y e. B x <_ y -> ( x e. A -> A. y e. B x <_ y ) )
46 elinel2 
 |-  ( w e. ( A i^i B ) -> w e. B )
47 breq2 
 |-  ( y = w -> ( x <_ y <-> x <_ w ) )
48 47 rspccv 
 |-  ( A. y e. B x <_ y -> ( w e. B -> x <_ w ) )
49 46 48 syl5 
 |-  ( A. y e. B x <_ y -> ( w e. ( A i^i B ) -> x <_ w ) )
50 45 49 syl6 
 |-  ( A. x e. A A. y e. B x <_ y -> ( x e. A -> ( w e. ( A i^i B ) -> x <_ w ) ) )
51 50 com23 
 |-  ( A. x e. A A. y e. B x <_ y -> ( w e. ( A i^i B ) -> ( x e. A -> x <_ w ) ) )
52 51 imp32 
 |-  ( ( A. x e. A A. y e. B x <_ y /\ ( w e. ( A i^i B ) /\ x e. A ) ) -> x <_ w )
53 52 3ad2antl3 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) ) -> x <_ w )
54 53 adantr 
 |-  ( ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) ) /\ y e. B ) -> x <_ w )
55 simp3 
 |-  ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> A. x e. A A. y e. B x <_ y )
56 30 adantr 
 |-  ( ( w e. ( A i^i B ) /\ x e. A ) -> w e. A )
57 breq1 
 |-  ( x = w -> ( x <_ y <-> w <_ y ) )
58 57 ralbidv 
 |-  ( x = w -> ( A. y e. B x <_ y <-> A. y e. B w <_ y ) )
59 58 rspccva 
 |-  ( ( A. x e. A A. y e. B x <_ y /\ w e. A ) -> A. y e. B w <_ y )
60 55 56 59 syl2an 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) ) -> A. y e. B w <_ y )
61 60 r19.21bi 
 |-  ( ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) ) /\ y e. B ) -> w <_ y )
62 54 61 jca 
 |-  ( ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) ) /\ y e. B ) -> ( x <_ w /\ w <_ y ) )
63 62 ex 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) ) -> ( y e. B -> ( x <_ w /\ w <_ y ) ) )
64 44 63 ralrimi 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ ( w e. ( A i^i B ) /\ x e. A ) ) -> A. y e. B ( x <_ w /\ w <_ y ) )
65 64 expr 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ w e. ( A i^i B ) ) -> ( x e. A -> A. y e. B ( x <_ w /\ w <_ y ) ) )
66 38 65 ralrimi 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ w e. ( A i^i B ) ) -> A. x e. A A. y e. B ( x <_ w /\ w <_ y ) )
67 breq2 
 |-  ( z = w -> ( x <_ z <-> x <_ w ) )
68 breq1 
 |-  ( z = w -> ( z <_ y <-> w <_ y ) )
69 67 68 anbi12d 
 |-  ( z = w -> ( ( x <_ z /\ z <_ y ) <-> ( x <_ w /\ w <_ y ) ) )
70 69 2ralbidv 
 |-  ( z = w -> ( A. x e. A A. y e. B ( x <_ z /\ z <_ y ) <-> A. x e. A A. y e. B ( x <_ w /\ w <_ y ) ) )
71 70 rspcev 
 |-  ( ( w e. RR /\ A. x e. A A. y e. B ( x <_ w /\ w <_ y ) ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
72 32 66 71 syl2anc 
 |-  ( ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) /\ w e. ( A i^i B ) ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
73 72 expcom 
 |-  ( w e. ( A i^i B ) -> ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) )
74 73 exlimiv 
 |-  ( E. w w e. ( A i^i B ) -> ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) )
75 28 74 sylbi 
 |-  ( ( A i^i B ) =/= (/) -> ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) )
76 27 75 pm2.61ine 
 |-  ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )