Proof of Theorem genpv
Step | Hyp | Ref
| Expression |
1 | | oveq1 7278 |
. . . 4
⊢ (𝑓 = 𝐴 → (𝑓𝐹𝑔) = (𝐴𝐹𝑔)) |
2 | | rexeq 3342 |
. . . . 5
⊢ (𝑓 = 𝐴 → (∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧))) |
3 | 2 | abbidv 2809 |
. . . 4
⊢ (𝑓 = 𝐴 → {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)}) |
4 | 1, 3 | eqeq12d 2756 |
. . 3
⊢ (𝑓 = 𝐴 → ((𝑓𝐹𝑔) = {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} ↔ (𝐴𝐹𝑔) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)})) |
5 | | oveq2 7279 |
. . . 4
⊢ (𝑔 = 𝐵 → (𝐴𝐹𝑔) = (𝐴𝐹𝐵)) |
6 | | rexeq 3342 |
. . . . . 6
⊢ (𝑔 = 𝐵 → (∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧))) |
7 | 6 | rexbidv 3228 |
. . . . 5
⊢ (𝑔 = 𝐵 → (∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧))) |
8 | 7 | abbidv 2809 |
. . . 4
⊢ (𝑔 = 𝐵 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧)}) |
9 | 5, 8 | eqeq12d 2756 |
. . 3
⊢ (𝑔 = 𝐵 → ((𝐴𝐹𝑔) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} ↔ (𝐴𝐹𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧)})) |
10 | | elprnq 10748 |
. . . . . . . . 9
⊢ ((𝑓 ∈ P ∧
𝑦 ∈ 𝑓) → 𝑦 ∈ Q) |
11 | | elprnq 10748 |
. . . . . . . . 9
⊢ ((𝑔 ∈ P ∧
𝑧 ∈ 𝑔) → 𝑧 ∈ Q) |
12 | | genp.2 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) |
13 | | eleq1 2828 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦𝐺𝑧) → (𝑥 ∈ Q ↔ (𝑦𝐺𝑧) ∈ Q)) |
14 | 12, 13 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
15 | 10, 11, 14 | syl2an 596 |
. . . . . . . 8
⊢ (((𝑓 ∈ P ∧
𝑦 ∈ 𝑓) ∧ (𝑔 ∈ P ∧ 𝑧 ∈ 𝑔)) → (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
16 | 15 | an4s 657 |
. . . . . . 7
⊢ (((𝑓 ∈ P ∧
𝑔 ∈ P)
∧ (𝑦 ∈ 𝑓 ∧ 𝑧 ∈ 𝑔)) → (𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
17 | 16 | rexlimdvva 3225 |
. . . . . 6
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (∃𝑦 ∈
𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧) → 𝑥 ∈ Q)) |
18 | 17 | abssdv 4007 |
. . . . 5
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∣
∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} ⊆ Q) |
19 | | nqex 10680 |
. . . . 5
⊢
Q ∈ V |
20 | | ssexg 5251 |
. . . . 5
⊢ (({𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} ⊆ Q ∧
Q ∈ V) → {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} ∈ V) |
21 | 18, 19, 20 | sylancl 586 |
. . . 4
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ {𝑥 ∣
∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} ∈ V) |
22 | | rexeq 3342 |
. . . . . 6
⊢ (𝑤 = 𝑓 → (∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧))) |
23 | 22 | abbidv 2809 |
. . . . 5
⊢ (𝑤 = 𝑓 → {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)}) |
24 | | rexeq 3342 |
. . . . . . 7
⊢ (𝑣 = 𝑔 → (∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧))) |
25 | 24 | rexbidv 3228 |
. . . . . 6
⊢ (𝑣 = 𝑔 → (∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧))) |
26 | 25 | abbidv 2809 |
. . . . 5
⊢ (𝑣 = 𝑔 → {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)} = {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)}) |
27 | | genp.1 |
. . . . 5
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)}) |
28 | 23, 26, 27 | ovmpog 7426 |
. . . 4
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ {𝑥 ∣
∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)} ∈ V) → (𝑓𝐹𝑔) = {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)}) |
29 | 21, 28 | mpd3an3 1461 |
. . 3
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓𝐹𝑔) = {𝑥 ∣ ∃𝑦 ∈ 𝑓 ∃𝑧 ∈ 𝑔 𝑥 = (𝑦𝐺𝑧)}) |
30 | 4, 9, 29 | vtocl2ga 3513 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧)}) |
31 | | eqeq1 2744 |
. . . . 5
⊢ (𝑥 = 𝑓 → (𝑥 = (𝑦𝐺𝑧) ↔ 𝑓 = (𝑦𝐺𝑧))) |
32 | 31 | 2rexbidv 3231 |
. . . 4
⊢ (𝑥 = 𝑓 → (∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑓 = (𝑦𝐺𝑧))) |
33 | | oveq1 7278 |
. . . . . 6
⊢ (𝑦 = 𝑔 → (𝑦𝐺𝑧) = (𝑔𝐺𝑧)) |
34 | 33 | eqeq2d 2751 |
. . . . 5
⊢ (𝑦 = 𝑔 → (𝑓 = (𝑦𝐺𝑧) ↔ 𝑓 = (𝑔𝐺𝑧))) |
35 | | oveq2 7279 |
. . . . . 6
⊢ (𝑧 = ℎ → (𝑔𝐺𝑧) = (𝑔𝐺ℎ)) |
36 | 35 | eqeq2d 2751 |
. . . . 5
⊢ (𝑧 = ℎ → (𝑓 = (𝑔𝐺𝑧) ↔ 𝑓 = (𝑔𝐺ℎ))) |
37 | 34, 36 | cbvrex2vw 3395 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝑓 = (𝑦𝐺𝑧) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ)) |
38 | 32, 37 | bitrdi 287 |
. . 3
⊢ (𝑥 = 𝑓 → (∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ))) |
39 | 38 | cbvabv 2813 |
. 2
⊢ {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦𝐺𝑧)} = {𝑓 ∣ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ)} |
40 | 30, 39 | eqtrdi 2796 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) = {𝑓 ∣ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ)}) |