Proof of Theorem recexprlemelu
Step | Hyp | Ref
| Expression |
1 | | elex 2741 |
. 2
⊢ (𝐶 ∈ (2nd
‘𝐵) → 𝐶 ∈ V) |
2 | | ltrelnq 7314 |
. . . . . . 7
⊢
<Q ⊆ (Q ×
Q) |
3 | 2 | brel 4661 |
. . . . . 6
⊢ (𝑦 <Q
𝐶 → (𝑦 ∈ Q ∧
𝐶 ∈
Q)) |
4 | 3 | simprd 113 |
. . . . 5
⊢ (𝑦 <Q
𝐶 → 𝐶 ∈ Q) |
5 | | elex 2741 |
. . . . 5
⊢ (𝐶 ∈ Q →
𝐶 ∈
V) |
6 | 4, 5 | syl 14 |
. . . 4
⊢ (𝑦 <Q
𝐶 → 𝐶 ∈ V) |
7 | 6 | adantr 274 |
. . 3
⊢ ((𝑦 <Q
𝐶 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) → 𝐶 ∈ V) |
8 | 7 | exlimiv 1591 |
. 2
⊢
(∃𝑦(𝑦 <Q
𝐶 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) → 𝐶 ∈ V) |
9 | | breq2 3991 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝑦 <Q 𝑥 ↔ 𝑦 <Q 𝐶)) |
10 | 9 | anbi1d 462 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) ↔ (𝑦 <Q 𝐶 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)))) |
11 | 10 | exbidv 1818 |
. . 3
⊢ (𝑥 = 𝐶 → (∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)))) |
12 | | recexpr.1 |
. . . . 5
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))}〉 |
13 | 12 | fveq2i 5497 |
. . . 4
⊢
(2nd ‘𝐵) = (2nd ‘〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))}〉) |
14 | | nqex 7312 |
. . . . . 6
⊢
Q ∈ V |
15 | 2 | brel 4661 |
. . . . . . . . . 10
⊢ (𝑥 <Q
𝑦 → (𝑥 ∈ Q ∧
𝑦 ∈
Q)) |
16 | 15 | simpld 111 |
. . . . . . . . 9
⊢ (𝑥 <Q
𝑦 → 𝑥 ∈ Q) |
17 | 16 | adantr 274 |
. . . . . . . 8
⊢ ((𝑥 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) → 𝑥 ∈ Q) |
18 | 17 | exlimiv 1591 |
. . . . . . 7
⊢
(∃𝑦(𝑥 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) → 𝑥 ∈ Q) |
19 | 18 | abssi 3222 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))} ⊆
Q |
20 | 14, 19 | ssexi 4125 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))} ∈ V |
21 | 2 | brel 4661 |
. . . . . . . . . 10
⊢ (𝑦 <Q
𝑥 → (𝑦 ∈ Q ∧
𝑥 ∈
Q)) |
22 | 21 | simprd 113 |
. . . . . . . . 9
⊢ (𝑦 <Q
𝑥 → 𝑥 ∈ Q) |
23 | 22 | adantr 274 |
. . . . . . . 8
⊢ ((𝑦 <Q
𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) → 𝑥 ∈ Q) |
24 | 23 | exlimiv 1591 |
. . . . . . 7
⊢
(∃𝑦(𝑦 <Q
𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) → 𝑥 ∈ Q) |
25 | 24 | abssi 3222 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))} ⊆
Q |
26 | 14, 25 | ssexi 4125 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))} ∈ V |
27 | 20, 26 | op2nd 6123 |
. . . 4
⊢
(2nd ‘〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))}〉) = {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))} |
28 | 13, 27 | eqtri 2191 |
. . 3
⊢
(2nd ‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))} |
29 | 11, 28 | elab2g 2877 |
. 2
⊢ (𝐶 ∈ V → (𝐶 ∈ (2nd
‘𝐵) ↔
∃𝑦(𝑦 <Q 𝐶 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)))) |
30 | 1, 8, 29 | pm5.21nii 699 |
1
⊢ (𝐶 ∈ (2nd
‘𝐵) ↔
∃𝑦(𝑦 <Q 𝐶 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))) |