Step | Hyp | Ref
| Expression |
1 | | ltrelpr 6488 |
. . . . . . . . 9
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 4335 |
. . . . . . . 8
⊢ (A<P B → (A
∈ P ∧ B ∈ P)) |
3 | | ltdfpr 6489 |
. . . . . . . . 9
⊢
((A ∈ P ∧ B ∈ P) → (A<P B ↔ ∃y ∈ Q (y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B)))) |
4 | 3 | biimpd 132 |
. . . . . . . 8
⊢
((A ∈ P ∧ B ∈ P) → (A<P B → ∃y ∈ Q (y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B)))) |
5 | 2, 4 | mpcom 32 |
. . . . . . 7
⊢ (A<P B → ∃y ∈ Q (y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B))) |
6 | | simprrl 491 |
. . . . . . . . . 10
⊢
((A<P
B ∧
(y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B)))) → y
∈ (2nd ‘A)) |
7 | 2 | simprd 107 |
. . . . . . . . . . . . 13
⊢ (A<P B → B ∈ P) |
8 | | prop 6458 |
. . . . . . . . . . . . . . . . . 18
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
9 | | prnmaxl 6471 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ y ∈ (1st ‘B)) → ∃w ∈ (1st ‘B)y
<Q w) |
10 | 8, 9 | sylan 267 |
. . . . . . . . . . . . . . . . 17
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w ∈ (1st ‘B)y
<Q w) |
11 | | ltexnqi 6392 |
. . . . . . . . . . . . . . . . . 18
⊢ (y <Q w → ∃𝑞 ∈ Q (y +Q 𝑞) = w) |
12 | 11 | reximi 2410 |
. . . . . . . . . . . . . . . . 17
⊢ (∃w ∈ (1st ‘B)y
<Q w →
∃w ∈ (1st ‘B)∃𝑞 ∈ Q (y +Q 𝑞) = w) |
13 | 10, 12 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w ∈ (1st ‘B)∃𝑞 ∈ Q (y +Q 𝑞) = w) |
14 | | df-rex 2306 |
. . . . . . . . . . . . . . . 16
⊢ (∃w ∈ (1st ‘B)∃𝑞 ∈ Q (y +Q 𝑞) = w
↔ ∃w(w ∈ (1st ‘B) ∧ ∃𝑞 ∈
Q (y
+Q 𝑞)
= w)) |
15 | 13, 14 | sylib 127 |
. . . . . . . . . . . . . . 15
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w(w ∈
(1st ‘B) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) = w)) |
16 | | r19.42v 2461 |
. . . . . . . . . . . . . . . 16
⊢ (∃𝑞 ∈
Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w)
↔ (w ∈ (1st ‘B) ∧ ∃𝑞 ∈
Q (y
+Q 𝑞)
= w)) |
17 | 16 | exbii 1493 |
. . . . . . . . . . . . . . 15
⊢ (∃w∃𝑞 ∈
Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w)
↔ ∃w(w ∈ (1st ‘B) ∧ ∃𝑞 ∈
Q (y
+Q 𝑞)
= w)) |
18 | 15, 17 | sylibr 137 |
. . . . . . . . . . . . . 14
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w∃𝑞 ∈
Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w)) |
19 | | eleq1 2097 |
. . . . . . . . . . . . . . . . 17
⊢
((y +Q
𝑞) = w → ((y
+Q 𝑞)
∈ (1st ‘B) ↔ w
∈ (1st ‘B))) |
20 | 19 | biimparc 283 |
. . . . . . . . . . . . . . . 16
⊢
((w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w)
→ (y +Q 𝑞) ∈ (1st ‘B)) |
21 | 20 | reximi 2410 |
. . . . . . . . . . . . . . 15
⊢ (∃𝑞 ∈
Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w)
→ ∃𝑞 ∈
Q (y
+Q 𝑞)
∈ (1st ‘B)) |
22 | 21 | exlimiv 1486 |
. . . . . . . . . . . . . 14
⊢ (∃w∃𝑞 ∈
Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w)
→ ∃𝑞 ∈
Q (y
+Q 𝑞)
∈ (1st ‘B)) |
23 | 18, 22 | syl 14 |
. . . . . . . . . . . . 13
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → ∃𝑞 ∈ Q (y +Q 𝑞) ∈
(1st ‘B)) |
24 | 7, 23 | sylan 267 |
. . . . . . . . . . . 12
⊢
((A<P
B ∧
y ∈
(1st ‘B)) → ∃𝑞 ∈
Q (y
+Q 𝑞)
∈ (1st ‘B)) |
25 | 24 | adantrl 447 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
(y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B))) → ∃𝑞 ∈
Q (y
+Q 𝑞)
∈ (1st ‘B)) |
26 | 25 | adantrl 447 |
. . . . . . . . . 10
⊢
((A<P
B ∧
(y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B)))) → ∃𝑞 ∈
Q (y
+Q 𝑞)
∈ (1st ‘B)) |
27 | 6, 26 | jca 290 |
. . . . . . . . 9
⊢
((A<P
B ∧
(y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B)))) → (y
∈ (2nd ‘A) ∧ ∃𝑞 ∈
Q (y
+Q 𝑞)
∈ (1st ‘B))) |
28 | 27 | expr 357 |
. . . . . . . 8
⊢
((A<P
B ∧
y ∈
Q) → ((y ∈ (2nd ‘A) ∧ y ∈
(1st ‘B)) → (y ∈
(2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈
(1st ‘B)))) |
29 | 28 | reximdva 2415 |
. . . . . . 7
⊢ (A<P B → (∃y ∈ Q (y ∈
(2nd ‘A) ∧ y ∈ (1st ‘B)) → ∃y ∈ Q (y ∈
(2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈
(1st ‘B)))) |
30 | 5, 29 | mpd 13 |
. . . . . 6
⊢ (A<P B → ∃y ∈ Q (y ∈
(2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈
(1st ‘B))) |
31 | | r19.42v 2461 |
. . . . . . 7
⊢ (∃𝑞 ∈
Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ (y ∈
(2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈
(1st ‘B))) |
32 | 31 | rexbii 2325 |
. . . . . 6
⊢ (∃y ∈ Q ∃𝑞 ∈
Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ ∃y ∈ Q (y ∈
(2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈
(1st ‘B))) |
33 | 30, 32 | sylibr 137 |
. . . . 5
⊢ (A<P B → ∃y ∈ Q ∃𝑞 ∈
Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B))) |
34 | | rexcom 2468 |
. . . . 5
⊢ (∃y ∈ Q ∃𝑞 ∈
Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ ∃𝑞 ∈
Q ∃y ∈
Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B))) |
35 | 33, 34 | sylib 127 |
. . . 4
⊢ (A<P B → ∃𝑞 ∈ Q ∃y ∈ Q (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))) |
36 | 2 | simpld 105 |
. . . . . . . . . . . 12
⊢ (A<P B → A ∈ P) |
37 | | prop 6458 |
. . . . . . . . . . . . 13
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
38 | | elprnqu 6465 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
39 | 37, 38 | sylan 267 |
. . . . . . . . . . . 12
⊢
((A ∈ P ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
40 | 36, 39 | sylan 267 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
y ∈
(2nd ‘A)) → y ∈
Q) |
41 | 40 | ex 108 |
. . . . . . . . . 10
⊢ (A<P B → (y
∈ (2nd ‘A) → y
∈ Q)) |
42 | 41 | pm4.71rd 374 |
. . . . . . . . 9
⊢ (A<P B → (y
∈ (2nd ‘A) ↔ (y
∈ Q ∧ y ∈ (2nd ‘A)))) |
43 | 42 | anbi1d 438 |
. . . . . . . 8
⊢ (A<P B → ((y
∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔
((y ∈
Q ∧ y ∈
(2nd ‘A)) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
44 | | anass 381 |
. . . . . . . 8
⊢
(((y ∈ Q ∧ y ∈ (2nd ‘A)) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ (y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
45 | 43, 44 | syl6bb 185 |
. . . . . . 7
⊢ (A<P B → ((y
∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ (y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))))) |
46 | 45 | exbidv 1703 |
. . . . . 6
⊢ (A<P B → (∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ↔ ∃y(y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))))) |
47 | 46 | rexbidv 2321 |
. . . . 5
⊢ (A<P B → (∃𝑞 ∈ Q ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q ∃y(y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))))) |
48 | | df-rex 2306 |
. . . . . 6
⊢ (∃y ∈ Q (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ↔ ∃y(y ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
49 | 48 | rexbii 2325 |
. . . . 5
⊢ (∃𝑞 ∈
Q ∃y ∈
Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ ∃𝑞 ∈
Q ∃y(y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)))) |
50 | 47, 49 | syl6bbr 187 |
. . . 4
⊢ (A<P B → (∃𝑞 ∈ Q ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q ∃y ∈ Q (y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
51 | 35, 50 | mpbird 156 |
. . 3
⊢ (A<P B → ∃𝑞 ∈ Q ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))) |
52 | | ltexprlem.1 |
. . . . . 6
⊢ 𝐶 = 〈{x ∈
Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈
(1st ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈
(2nd ‘B))}〉 |
53 | 52 | ltexprlemell 6572 |
. . . . 5
⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
54 | 53 | rexbii 2325 |
. . . 4
⊢ (∃𝑞 ∈
Q 𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑞 ∈
Q (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)))) |
55 | | ssid 2958 |
. . . . 5
⊢
Q ⊆ Q |
56 | | rexss 3001 |
. . . . 5
⊢
(Q ⊆ Q → (∃𝑞 ∈
Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ ∃𝑞 ∈
Q (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B))))) |
57 | 55, 56 | ax-mp 7 |
. . . 4
⊢ (∃𝑞 ∈
Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ↔ ∃𝑞 ∈
Q (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)))) |
58 | 54, 57 | bitr4i 176 |
. . 3
⊢ (∃𝑞 ∈
Q 𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑞 ∈
Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B))) |
59 | 51, 58 | sylibr 137 |
. 2
⊢ (A<P B → ∃𝑞 ∈ Q 𝑞 ∈
(1st ‘𝐶)) |
60 | | nfv 1418 |
. . 3
⊢
Ⅎ𝑟 A<P B |
61 | | nfre1 2359 |
. . 3
⊢
Ⅎ𝑟∃𝑟 ∈
Q 𝑟 ∈ (2nd ‘𝐶) |
62 | | prmu 6461 |
. . . . 5
⊢
(〈(1st ‘B),
(2nd ‘B)〉 ∈ P → ∃𝑟 ∈
Q 𝑟 ∈ (2nd ‘B)) |
63 | | rexex 2362 |
. . . . 5
⊢ (∃𝑟 ∈
Q 𝑟 ∈ (2nd ‘B) → ∃𝑟 𝑟 ∈
(2nd ‘B)) |
64 | 62, 63 | syl 14 |
. . . 4
⊢
(〈(1st ‘B),
(2nd ‘B)〉 ∈ P → ∃𝑟 𝑟 ∈
(2nd ‘B)) |
65 | 7, 8, 64 | 3syl 17 |
. . 3
⊢ (A<P B → ∃𝑟 𝑟 ∈
(2nd ‘B)) |
66 | | elprnqu 6465 |
. . . . . . 7
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ 𝑟
∈ (2nd ‘B)) → 𝑟 ∈
Q) |
67 | 8, 66 | sylan 267 |
. . . . . 6
⊢
((B ∈ P ∧ 𝑟
∈ (2nd ‘B)) → 𝑟 ∈
Q) |
68 | 7, 67 | sylan 267 |
. . . . 5
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B)) → 𝑟 ∈
Q) |
69 | | prml 6460 |
. . . . . . . . 9
⊢
(〈(1st ‘A),
(2nd ‘A)〉 ∈ P → ∃y ∈ Q y ∈
(1st ‘A)) |
70 | 37, 69 | syl 14 |
. . . . . . . 8
⊢ (A ∈
P → ∃y ∈
Q y ∈ (1st ‘A)) |
71 | | rexex 2362 |
. . . . . . . 8
⊢ (∃y ∈ Q y ∈
(1st ‘A) → ∃y y ∈
(1st ‘A)) |
72 | 36, 70, 71 | 3syl 17 |
. . . . . . 7
⊢ (A<P B → ∃y y ∈
(1st ‘A)) |
73 | 72 | adantr 261 |
. . . . . 6
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B)) → ∃y y ∈
(1st ‘A)) |
74 | 68 | 3adant3 923 |
. . . . . . . . 9
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → 𝑟 ∈ Q) |
75 | | simp3 905 |
. . . . . . . . . 10
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → y ∈
(1st ‘A)) |
76 | | elprnql 6464 |
. . . . . . . . . . . . . . 15
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ y ∈ (1st ‘A)) → y
∈ Q) |
77 | 37, 76 | sylan 267 |
. . . . . . . . . . . . . 14
⊢
((A ∈ P ∧ y ∈ (1st ‘A)) → y
∈ Q) |
78 | 36, 77 | sylan 267 |
. . . . . . . . . . . . 13
⊢
((A<P
B ∧
y ∈
(1st ‘A)) → y ∈
Q) |
79 | 78 | 3adant2 922 |
. . . . . . . . . . . 12
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → y ∈
Q) |
80 | | addcomnqg 6365 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ Q ∧ y ∈ Q) → (𝑟 +Q y) = (y
+Q 𝑟)) |
81 | 74, 79, 80 | syl2anc 391 |
. . . . . . . . . . 11
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → (𝑟 +Q
y) = (y
+Q 𝑟)) |
82 | | ltaddnq 6390 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ Q ∧ y ∈ Q) → 𝑟 <Q (𝑟 +Q
y)) |
83 | 74, 79, 82 | syl2anc 391 |
. . . . . . . . . . . 12
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → 𝑟 <Q
(𝑟 +Q
y)) |
84 | | prcunqu 6468 |
. . . . . . . . . . . . . . 15
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ 𝑟
∈ (2nd ‘B)) → (𝑟 <Q (𝑟 +Q
y) → (𝑟 +Q y) ∈
(2nd ‘B))) |
85 | 8, 84 | sylan 267 |
. . . . . . . . . . . . . 14
⊢
((B ∈ P ∧ 𝑟
∈ (2nd ‘B)) → (𝑟 <Q (𝑟 +Q
y) → (𝑟 +Q y) ∈
(2nd ‘B))) |
86 | 7, 85 | sylan 267 |
. . . . . . . . . . . . 13
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B)) → (𝑟 <Q (𝑟 +Q
y) → (𝑟 +Q y) ∈
(2nd ‘B))) |
87 | 86 | 3adant3 923 |
. . . . . . . . . . . 12
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → (𝑟 <Q
(𝑟 +Q
y) → (𝑟 +Q y) ∈
(2nd ‘B))) |
88 | 83, 87 | mpd 13 |
. . . . . . . . . . 11
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → (𝑟 +Q
y) ∈
(2nd ‘B)) |
89 | 81, 88 | eqeltrrd 2112 |
. . . . . . . . . 10
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → (y +Q 𝑟) ∈
(2nd ‘B)) |
90 | | 19.8a 1479 |
. . . . . . . . . 10
⊢
((y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)) → ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B))) |
91 | 75, 89, 90 | syl2anc 391 |
. . . . . . . . 9
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B))) |
92 | 74, 91 | jca 290 |
. . . . . . . 8
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) |
93 | 52 | ltexprlemelu 6573 |
. . . . . . . 8
⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈
Q ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B)))) |
94 | 92, 93 | sylibr 137 |
. . . . . . 7
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈
(1st ‘A)) → 𝑟 ∈ (2nd ‘𝐶)) |
95 | 94 | 3expa 1103 |
. . . . . 6
⊢
(((A<P
B ∧ 𝑟 ∈ (2nd ‘B)) ∧ y ∈
(1st ‘A)) → 𝑟 ∈ (2nd ‘𝐶)) |
96 | 73, 95 | exlimddv 1775 |
. . . . 5
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B)) → 𝑟 ∈
(2nd ‘𝐶)) |
97 | | 19.8a 1479 |
. . . . 5
⊢ ((𝑟 ∈ Q ∧ 𝑟
∈ (2nd ‘𝐶)) → ∃𝑟(𝑟 ∈
Q ∧ 𝑟 ∈
(2nd ‘𝐶))) |
98 | 68, 96, 97 | syl2anc 391 |
. . . 4
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B)) → ∃𝑟(𝑟 ∈
Q ∧ 𝑟 ∈
(2nd ‘𝐶))) |
99 | | df-rex 2306 |
. . . 4
⊢ (∃𝑟 ∈
Q 𝑟 ∈ (2nd ‘𝐶) ↔ ∃𝑟(𝑟 ∈
Q ∧ 𝑟 ∈
(2nd ‘𝐶))) |
100 | 98, 99 | sylibr 137 |
. . 3
⊢
((A<P
B ∧ 𝑟 ∈ (2nd ‘B)) → ∃𝑟 ∈ Q 𝑟 ∈
(2nd ‘𝐶)) |
101 | 60, 61, 65, 100 | exlimdd 1749 |
. 2
⊢ (A<P B → ∃𝑟 ∈ Q 𝑟 ∈
(2nd ‘𝐶)) |
102 | 59, 101 | jca 290 |
1
⊢ (A<P B → (∃𝑞 ∈ Q 𝑞 ∈
(1st ‘𝐶)
∧ ∃𝑟 ∈ Q 𝑟 ∈
(2nd ‘𝐶))) |