Step | Hyp | Ref
| Expression |
1 | | df-pg 47467 |
. 2
⊢ Pg =
setrecs((𝑎 ∈ V ↦
(𝒫 𝑎 ×
𝒫 𝑎))) |
2 | | pgindnf.4 |
. 2
⊢ (𝑦 = 𝐴 → (𝜒 ↔ 𝜃)) |
3 | | pgindnf.1 |
. . . . . . 7
⊢
Ⅎ𝑥𝜑 |
4 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑦 ∈ 𝑧 𝜒 |
5 | 3, 4 | nfan 1902 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) |
6 | | pgindlem 47472 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → ((1st
‘𝑥) ∪
(2nd ‘𝑥))
⊆ 𝑧) |
7 | 6 | sseld 3978 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → (𝑦 ∈ ((1st ‘𝑥) ∪ (2nd
‘𝑥)) → 𝑦 ∈ 𝑧)) |
8 | 7 | imim1d 82 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → ((𝑦 ∈ 𝑧 → 𝜒) → (𝑦 ∈ ((1st ‘𝑥) ∪ (2nd
‘𝑥)) → 𝜒))) |
9 | 8 | ralimdv2 3163 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → (∀𝑦 ∈ 𝑧 𝜒 → ∀𝑦 ∈ ((1st ‘𝑥) ∪ (2nd
‘𝑥))𝜒)) |
10 | | pgindnf.5 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥(∀𝑦 ∈ ((1st ‘𝑥) ∪ (2nd
‘𝑥))𝜒 → 𝜓)) |
11 | 10 | 19.21bi 2182 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑦 ∈ ((1st
‘𝑥) ∪
(2nd ‘𝑥))𝜒 → 𝜓)) |
12 | 9, 11 | sylan9r 509 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧)) → (∀𝑦 ∈ 𝑧 𝜒 → 𝜓)) |
13 | 12 | impancom 452 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) → (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → 𝜓)) |
14 | 5, 13 | ralrimi 3254 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) → ∀𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧)𝜓) |
15 | | pgindnf.3 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) |
16 | | vex 3478 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
17 | | pweq 4611 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑧 → 𝒫 𝑎 = 𝒫 𝑧) |
18 | 17 | sqxpeqd 5702 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑧 → (𝒫 𝑎 × 𝒫 𝑎) = (𝒫 𝑧 × 𝒫 𝑧)) |
19 | | eqid 2732 |
. . . . . . . . . 10
⊢ (𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎)) = (𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎)) |
20 | | vpwex 5369 |
. . . . . . . . . . 11
⊢ 𝒫
𝑧 ∈ V |
21 | 20, 20 | xpex 7724 |
. . . . . . . . . 10
⊢
(𝒫 𝑧 ×
𝒫 𝑧) ∈
V |
22 | 18, 19, 21 | fvmpt 6985 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → ((𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎))‘𝑧) = (𝒫 𝑧 × 𝒫 𝑧)) |
23 | 16, 22 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎))‘𝑧) = (𝒫 𝑧 × 𝒫 𝑧) |
24 | 23 | eqcomi 2741 |
. . . . . . 7
⊢
(𝒫 𝑧 ×
𝒫 𝑧) = ((𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎))‘𝑧) |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝒫 𝑧 × 𝒫 𝑧) = ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)) |
26 | 15, 25 | cbvralv2 3939 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝑧 ×
𝒫 𝑧)𝜓 ↔ ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒) |
27 | 14, 26 | sylib 217 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) → ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒) |
28 | 27 | ex 413 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝑧 𝜒 → ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒)) |
29 | 28 | alrimiv 1930 |
. 2
⊢ (𝜑 → ∀𝑧(∀𝑦 ∈ 𝑧 𝜒 → ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒)) |
30 | 1, 2, 29 | setis 47455 |
1
⊢ (𝜑 → (𝐴 ∈ Pg → 𝜃)) |