Proof of Theorem genpdf
Step | Hyp | Ref
| Expression |
1 | | genpdf.1 |
. 2
⊢ 𝐹 = (w ∈
P, v ∈ P ↦ 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘w) ∧ 𝑠 ∈ (1st ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘w) ∧ 𝑠 ∈ (2nd ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))}〉) |
2 | | prop 6458 |
. . . . . . 7
⊢ (w ∈
P → 〈(1st ‘w), (2nd ‘w)〉 ∈
P) |
3 | | elprnql 6464 |
. . . . . . 7
⊢
((〈(1st ‘w),
(2nd ‘w)〉 ∈ P ∧ 𝑟
∈ (1st ‘w)) → 𝑟 ∈
Q) |
4 | 2, 3 | sylan 267 |
. . . . . 6
⊢
((w ∈ P ∧ 𝑟
∈ (1st ‘w)) → 𝑟 ∈
Q) |
5 | 4 | adantlr 446 |
. . . . 5
⊢
(((w ∈ P ∧ v ∈ P) ∧ 𝑟
∈ (1st ‘w)) → 𝑟 ∈
Q) |
6 | | prop 6458 |
. . . . . . 7
⊢ (v ∈
P → 〈(1st ‘v), (2nd ‘v)〉 ∈
P) |
7 | | elprnql 6464 |
. . . . . . 7
⊢
((〈(1st ‘v),
(2nd ‘v)〉 ∈ P ∧ 𝑠
∈ (1st ‘v)) → 𝑠 ∈
Q) |
8 | 6, 7 | sylan 267 |
. . . . . 6
⊢
((v ∈ P ∧ 𝑠
∈ (1st ‘v)) → 𝑠 ∈
Q) |
9 | 8 | adantll 445 |
. . . . 5
⊢
(((w ∈ P ∧ v ∈ P) ∧ 𝑠
∈ (1st ‘v)) → 𝑠 ∈
Q) |
10 | 5, 9 | genpdflem 6490 |
. . . 4
⊢
((w ∈ P ∧ v ∈ P) → {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘w) ∧ 𝑠 ∈ (1st ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈
Q ∣ ∃𝑟 ∈
(1st ‘w)∃𝑠 ∈
(1st ‘v)𝑞 = (𝑟𝐺𝑠)}) |
11 | | elprnqu 6465 |
. . . . . . 7
⊢
((〈(1st ‘w),
(2nd ‘w)〉 ∈ P ∧ 𝑟
∈ (2nd ‘w)) → 𝑟 ∈
Q) |
12 | 2, 11 | sylan 267 |
. . . . . 6
⊢
((w ∈ P ∧ 𝑟
∈ (2nd ‘w)) → 𝑟 ∈
Q) |
13 | 12 | adantlr 446 |
. . . . 5
⊢
(((w ∈ P ∧ v ∈ P) ∧ 𝑟
∈ (2nd ‘w)) → 𝑟 ∈
Q) |
14 | | elprnqu 6465 |
. . . . . . 7
⊢
((〈(1st ‘v),
(2nd ‘v)〉 ∈ P ∧ 𝑠
∈ (2nd ‘v)) → 𝑠 ∈
Q) |
15 | 6, 14 | sylan 267 |
. . . . . 6
⊢
((v ∈ P ∧ 𝑠
∈ (2nd ‘v)) → 𝑠 ∈
Q) |
16 | 15 | adantll 445 |
. . . . 5
⊢
(((w ∈ P ∧ v ∈ P) ∧ 𝑠
∈ (2nd ‘v)) → 𝑠 ∈
Q) |
17 | 13, 16 | genpdflem 6490 |
. . . 4
⊢
((w ∈ P ∧ v ∈ P) → {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘w) ∧ 𝑠 ∈ (2nd ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈
Q ∣ ∃𝑟 ∈
(2nd ‘w)∃𝑠 ∈
(2nd ‘v)𝑞 = (𝑟𝐺𝑠)}) |
18 | 10, 17 | opeq12d 3548 |
. . 3
⊢
((w ∈ P ∧ v ∈ P) → 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘w) ∧ 𝑠 ∈ (1st ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘w) ∧ 𝑠 ∈ (2nd ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))}〉 = 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
(1st ‘w)∃𝑠 ∈
(1st ‘v)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
(2nd ‘w)∃𝑠 ∈
(2nd ‘v)𝑞 = (𝑟𝐺𝑠)}〉) |
19 | 18 | mpt2eq3ia 5512 |
. 2
⊢ (w ∈
P, v ∈ P ↦ 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘w) ∧ 𝑠 ∈ (1st ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘w) ∧ 𝑠 ∈ (2nd ‘v) ∧ 𝑞 = (𝑟𝐺𝑠))}〉) = (w ∈
P, v ∈ P ↦ 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
(1st ‘w)∃𝑠 ∈
(1st ‘v)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
(2nd ‘w)∃𝑠 ∈
(2nd ‘v)𝑞 = (𝑟𝐺𝑠)}〉) |
20 | 1, 19 | eqtri 2057 |
1
⊢ 𝐹 = (w ∈
P, v ∈ P ↦ 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
(1st ‘w)∃𝑠 ∈
(1st ‘v)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
(2nd ‘w)∃𝑠 ∈
(2nd ‘v)𝑞 = (𝑟𝐺𝑠)}〉) |