| Step | Hyp | Ref
| Expression |
| 1 | | df-pg 49229 |
. 2
⊢ Pg =
setrecs((𝑎 ∈ V ↦
(𝒫 𝑎 ×
𝒫 𝑎))) |
| 2 | | pgindnf.4 |
. 2
⊢ (𝑦 = 𝐴 → (𝜒 ↔ 𝜃)) |
| 3 | | pgindnf.1 |
. . . . . . 7
⊢
Ⅎ𝑥𝜑 |
| 4 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑦 ∈ 𝑧 𝜒 |
| 5 | 3, 4 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) |
| 6 | | pgindlem 49234 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → ((1st
‘𝑥) ∪
(2nd ‘𝑥))
⊆ 𝑧) |
| 7 | 6 | sseld 3982 |
. . . . . . . . . 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 2189 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑦 ∈ ((1st
‘𝑥) ∪
(2nd ‘𝑥))𝜒 → 𝜓)) |
| 12 | 9, 11 | sylan9r 508 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧)) → (∀𝑦 ∈ 𝑧 𝜒 → 𝜓)) |
| 13 | 12 | impancom 451 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) → (𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧) → 𝜓)) |
| 14 | 5, 13 | ralrimi 3257 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) → ∀𝑥 ∈ (𝒫 𝑧 × 𝒫 𝑧)𝜓) |
| 15 | | pgindnf.3 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) |
| 16 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
| 17 | | pweq 4614 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑧 → 𝒫 𝑎 = 𝒫 𝑧) |
| 18 | 17 | sqxpeqd 5717 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑧 → (𝒫 𝑎 × 𝒫 𝑎) = (𝒫 𝑧 × 𝒫 𝑧)) |
| 19 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎)) = (𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎)) |
| 20 | | vpwex 5377 |
. . . . . . . . . . 11
⊢ 𝒫
𝑧 ∈ V |
| 21 | 20, 20 | xpex 7773 |
. . . . . . . . . 10
⊢
(𝒫 𝑧 ×
𝒫 𝑧) ∈
V |
| 22 | 18, 19, 21 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → ((𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎))‘𝑧) = (𝒫 𝑧 × 𝒫 𝑧)) |
| 23 | 16, 22 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎))‘𝑧) = (𝒫 𝑧 × 𝒫 𝑧) |
| 24 | 23 | eqcomi 2746 |
. . . . . . 7
⊢
(𝒫 𝑧 ×
𝒫 𝑧) = ((𝑎 ∈ V ↦ (𝒫
𝑎 × 𝒫 𝑎))‘𝑧) |
| 25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝒫 𝑧 × 𝒫 𝑧) = ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)) |
| 26 | 15, 25 | cbvralv2 3945 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝑧 ×
𝒫 𝑧)𝜓 ↔ ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒) |
| 27 | 14, 26 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑧 𝜒) → ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒) |
| 28 | 27 | ex 412 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝑧 𝜒 → ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒)) |
| 29 | 28 | alrimiv 1927 |
. 2
⊢ (𝜑 → ∀𝑧(∀𝑦 ∈ 𝑧 𝜒 → ∀𝑦 ∈ ((𝑎 ∈ V ↦ (𝒫 𝑎 × 𝒫 𝑎))‘𝑧)𝜒)) |
| 30 | 1, 2, 29 | setis 49217 |
1
⊢ (𝜑 → (𝐴 ∈ Pg → 𝜃)) |