Proof of Theorem genpdflem
Step | Hyp | Ref
| Expression |
1 | | genpdflem.r |
. . . . . . . . 9
⊢ ((φ ∧ 𝑟 ∈ A) →
𝑟 ∈ Q) |
2 | 1 | ex 108 |
. . . . . . . 8
⊢ (φ → (𝑟 ∈ A → 𝑟 ∈
Q)) |
3 | 2 | pm4.71rd 374 |
. . . . . . 7
⊢ (φ → (𝑟 ∈ A ↔ (𝑟 ∈
Q ∧ 𝑟 ∈ A))) |
4 | 3 | anbi1d 438 |
. . . . . 6
⊢ (φ → ((𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))) ↔ ((𝑟 ∈
Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))))) |
5 | 4 | exbidv 1703 |
. . . . 5
⊢ (φ → (∃𝑟(𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))) ↔ ∃𝑟((𝑟 ∈
Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))))) |
6 | | 3anass 888 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ (𝑟 ∈ A ∧ (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)))) |
7 | 6 | rexbii 2325 |
. . . . . . . . 9
⊢ (∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈
Q (𝑟 ∈ A ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))) |
8 | | r19.42v 2461 |
. . . . . . . . 9
⊢ (∃𝑠 ∈
Q (𝑟 ∈ A ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)))) |
9 | 7, 8 | bitri 173 |
. . . . . . . 8
⊢ (∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ (𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)))) |
10 | 9 | rexbii 2325 |
. . . . . . 7
⊢ (∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈
Q (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))) |
11 | | df-rex 2306 |
. . . . . . 7
⊢ (∃𝑟 ∈
Q (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈
Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))))) |
12 | 10, 11 | bitri 173 |
. . . . . 6
⊢ (∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈
Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))))) |
13 | | anass 381 |
. . . . . . 7
⊢ (((𝑟 ∈ Q ∧ 𝑟
∈ A)
∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈
Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))))) |
14 | 13 | exbii 1493 |
. . . . . 6
⊢ (∃𝑟((𝑟 ∈
Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈
Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))))) |
15 | 12, 14 | bitr4i 176 |
. . . . 5
⊢ (∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑟((𝑟 ∈
Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)))) |
16 | 5, 15 | syl6rbbr 188 |
. . . 4
⊢ (φ → (∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠))))) |
17 | | df-rex 2306 |
. . . 4
⊢ (∃𝑟 ∈ A ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ A ∧ ∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)))) |
18 | 16, 17 | syl6bbr 187 |
. . 3
⊢ (φ → (∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ A ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))) |
19 | | genpdflem.s |
. . . . . . . . . 10
⊢ ((φ ∧ 𝑠 ∈ B) →
𝑠 ∈ Q) |
20 | 19 | ex 108 |
. . . . . . . . 9
⊢ (φ → (𝑠 ∈ B → 𝑠 ∈
Q)) |
21 | 20 | pm4.71rd 374 |
. . . . . . . 8
⊢ (φ → (𝑠 ∈ B ↔ (𝑠 ∈
Q ∧ 𝑠 ∈ B))) |
22 | 21 | anbi1d 438 |
. . . . . . 7
⊢ (φ → ((𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ((𝑠 ∈
Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠)))) |
23 | 22 | exbidv 1703 |
. . . . . 6
⊢ (φ → (∃𝑠(𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈
Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠)))) |
24 | | df-rex 2306 |
. . . . . . 7
⊢ (∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈
Q ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))) |
25 | | anass 381 |
. . . . . . . 8
⊢ (((𝑠 ∈ Q ∧ 𝑠
∈ B)
∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑠 ∈
Q ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))) |
26 | 25 | exbii 1493 |
. . . . . . 7
⊢ (∃𝑠((𝑠 ∈
Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈
Q ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))) |
27 | 24, 26 | bitr4i 176 |
. . . . . 6
⊢ (∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈
Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠))) |
28 | 23, 27 | syl6rbbr 188 |
. . . . 5
⊢ (φ → (∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))) |
29 | | df-rex 2306 |
. . . . 5
⊢ (∃𝑠 ∈ B 𝑞
= (𝑟𝐺𝑠) ↔ ∃𝑠(𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) |
30 | 28, 29 | syl6bbr 187 |
. . . 4
⊢ (φ → (∃𝑠 ∈
Q (𝑠 ∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ B 𝑞
= (𝑟𝐺𝑠))) |
31 | 30 | rexbidv 2321 |
. . 3
⊢ (φ → (∃𝑟 ∈ A ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ A ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠))) |
32 | 18, 31 | bitrd 177 |
. 2
⊢ (φ → (∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ A ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠))) |
33 | 32 | rabbidv 2543 |
1
⊢ (φ → {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ A ∧ 𝑠
∈ B ∧ 𝑞
= (𝑟𝐺𝑠))} = {𝑞 ∈
Q ∣ ∃𝑟 ∈ A ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠)}) |