Metamath Proof Explorer

Theorem archiabllem2a

Description: Lemma for archiabl , which requires the group to be both left- and right-ordered. (Contributed by Thierry Arnoux, 13-Apr-2018)

Ref Expression
Hypotheses archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
archiabllem2.1 ⊢ + = ( +g ‘ 𝑊 )
archiabllem2.2 ⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
archiabllem2.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
archiabllem2a.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
archiabllem2a.5 ⊢ ( 𝜑 → 0 < 𝑋 )
Assertion archiabllem2a ( 𝜑 → ∃ 𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
4 archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
5 archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
6 archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
7 archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
8 archiabllem2.1 ⊢ + = ( +g ‘ 𝑊 )
9 archiabllem2.2 ⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
10 archiabllem2.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
11 archiabllem2a.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 archiabllem2a.5 ⊢ ( 𝜑 → 0 < 𝑋 )
13 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) ≤ 𝑋 ) → 𝑏 ∈ 𝐵 )
14 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) ≤ 𝑋 ) → 0 < 𝑏 )
15 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) ≤ 𝑋 ) → ( 𝑏 + 𝑏 ) ≤ 𝑋 )
16 breq2 ⊢ ( 𝑐 = 𝑏 → ( 0 < 𝑐 ↔ 0 < 𝑏 ) )
17 id ⊢ ( 𝑐 = 𝑏 → 𝑐 = 𝑏 )
18 17 17 oveq12d ⊢ ( 𝑐 = 𝑏 → ( 𝑐 + 𝑐 ) = ( 𝑏 + 𝑏 ) )
19 18 breq1d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑐 + 𝑐 ) ≤ 𝑋 ↔ ( 𝑏 + 𝑏 ) ≤ 𝑋 ) )
20 16 19 anbi12d ⊢ ( 𝑐 = 𝑏 → ( ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) ↔ ( 0 < 𝑏 ∧ ( 𝑏 + 𝑏 ) ≤ 𝑋 ) ) )
21 20 rspcev ⊢ ( ( 𝑏 ∈ 𝐵 ∧ ( 0 < 𝑏 ∧ ( 𝑏 + 𝑏 ) ≤ 𝑋 ) ) → ∃ 𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) )
22 13 14 15 21 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) ≤ 𝑋 ) → ∃ 𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) )
23 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝜑 )
24 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
25 23 6 24 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑊 ∈ Grp )
26 23 11 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑋 ∈ 𝐵 )
27 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑏 ∈ 𝐵 )
28 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
29 1 28 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ∈ 𝐵 )
30 25 26 27 29 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ∈ 𝐵 )
31 1 2 28 grpsubid ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( -g ‘ 𝑊 ) 𝑏 ) = 0 )
32 25 27 31 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 ( -g ‘ 𝑊 ) 𝑏 ) = 0 )
33 23 6 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑊 ∈ oGrp )
34 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑏 < 𝑋 )
35 1 4 28 ogrpsublt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 < 𝑋 ) → ( 𝑏 ( -g ‘ 𝑊 ) 𝑏 ) < ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) )
36 33 27 26 27 34 35 syl131anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 ( -g ‘ 𝑊 ) 𝑏 ) < ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) )
37 32 36 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 0 < ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) )
38 23 9 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( oppg ‘ 𝑊 ) ∈ oGrp )
39 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 + 𝑏 ) ∈ 𝐵 )
40 25 27 27 39 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 + 𝑏 ) ∈ 𝐵 )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑋 < ( 𝑏 + 𝑏 ) )
42 1 4 28 ogrpsublt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑏 + 𝑏 ) ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) < ( ( 𝑏 + 𝑏 ) ( -g ‘ 𝑊 ) 𝑏 ) )
43 33 26 40 27 41 42 syl131anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) < ( ( 𝑏 + 𝑏 ) ( -g ‘ 𝑊 ) 𝑏 ) )
44 1 8 28 grpaddsubass ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑏 + 𝑏 ) ( -g ‘ 𝑊 ) 𝑏 ) = ( 𝑏 + ( 𝑏 ( -g ‘ 𝑊 ) 𝑏 ) ) )
45 25 27 27 27 44 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑏 + 𝑏 ) ( -g ‘ 𝑊 ) 𝑏 ) = ( 𝑏 + ( 𝑏 ( -g ‘ 𝑊 ) 𝑏 ) ) )
46 32 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 + ( 𝑏 ( -g ‘ 𝑊 ) 𝑏 ) ) = ( 𝑏 + 0 ) )
47 1 8 2 grprid ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 + 0 ) = 𝑏 )
48 25 27 47 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 + 0 ) = 𝑏 )
49 45 46 48 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑏 + 𝑏 ) ( -g ‘ 𝑊 ) 𝑏 ) = 𝑏 )
50 43 49 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) < 𝑏 )
51 1 4 8 25 38 30 27 30 50 ogrpaddltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) < ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + 𝑏 ) )
52 1 8 28 grpnpcan ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + 𝑏 ) = 𝑋 )
53 25 26 27 52 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + 𝑏 ) = 𝑋 )
54 51 53 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) < 𝑋 )
55 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ∈ V )
56 3 4 pltle ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) < 𝑋 → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ≤ 𝑋 ) )
57 25 55 26 56 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) < 𝑋 → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ≤ 𝑋 ) )
58 54 57 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ≤ 𝑋 )
59 breq2 ⊢ ( 𝑐 = ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) → ( 0 < 𝑐 ↔ 0 < ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) )
60 id ⊢ ( 𝑐 = ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) → 𝑐 = ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) )
61 60 60 oveq12d ⊢ ( 𝑐 = ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) → ( 𝑐 + 𝑐 ) = ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) )
62 61 breq1d ⊢ ( 𝑐 = ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) → ( ( 𝑐 + 𝑐 ) ≤ 𝑋 ↔ ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ≤ 𝑋 ) )
63 59 62 anbi12d ⊢ ( 𝑐 = ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) → ( ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) ↔ ( 0 < ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ∧ ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ≤ 𝑋 ) ) )
64 63 rspcev ⊢ ( ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ∈ 𝐵 ∧ ( 0 < ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ∧ ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) + ( 𝑋 ( -g ‘ 𝑊 ) 𝑏 ) ) ≤ 𝑋 ) ) → ∃ 𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) )
65 30 37 58 64 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ∃ 𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) )
66 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → 𝑊 ∈ oGrp )
67 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
68 67 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
69 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
70 66 68 69 3syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → 𝑊 ∈ Toset )
71 66 24 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → 𝑊 ∈ Grp )
72 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → 𝑏 ∈ 𝐵 )
73 71 72 72 39 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → ( 𝑏 + 𝑏 ) ∈ 𝐵 )
74 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → 𝑋 ∈ 𝐵 )
75 1 3 4 tlt2 ⊢ ( ( 𝑊 ∈ Toset ∧ ( 𝑏 + 𝑏 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑏 + 𝑏 ) ≤ 𝑋 ∨ 𝑋 < ( 𝑏 + 𝑏 ) ) )
76 70 73 74 75 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → ( ( 𝑏 + 𝑏 ) ≤ 𝑋 ∨ 𝑋 < ( 𝑏 + 𝑏 ) ) )
77 22 65 76 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) → ∃ 𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) )
78 10 3expia ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 0 < 𝑎 → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ) )
79 78 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ( 0 < 𝑎 → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ) )
80 breq2 ⊢ ( 𝑎 = 𝑋 → ( 0 < 𝑎 ↔ 0 < 𝑋 ) )
81 breq2 ⊢ ( 𝑎 = 𝑋 → ( 𝑏 < 𝑎 ↔ 𝑏 < 𝑋 ) )
82 81 anbi2d ⊢ ( 𝑎 = 𝑋 → ( ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ↔ ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) )
83 82 rexbidv ⊢ ( 𝑎 = 𝑋 → ( ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ↔ ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) )
84 80 83 imbi12d ⊢ ( 𝑎 = 𝑋 → ( ( 0 < 𝑎 → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ) ↔ ( 0 < 𝑋 → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ) )
85 84 rspcv ⊢ ( 𝑋 ∈ 𝐵 → ( ∀ 𝑎 ∈ 𝐵 ( 0 < 𝑎 → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( 0 < 𝑋 → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) ) ) )
86 11 79 12 85 syl3c ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋 ) )
87 77 86 r19.29a ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) ≤ 𝑋 ) )