Proof of Theorem sprvalpwn0
| Step | Hyp | Ref
| Expression |
| 1 | | sprvalpw 47467 |
. 2
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}}) |
| 2 | | id 22 |
. . . . . . . . 9
⊢ (𝑝 = {𝑎, 𝑏} → 𝑝 = {𝑎, 𝑏}) |
| 3 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
| 4 | 3 | prnz 4777 |
. . . . . . . . . 10
⊢ {𝑎, 𝑏} ≠ ∅ |
| 5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝑝 = {𝑎, 𝑏} → {𝑎, 𝑏} ≠ ∅) |
| 6 | 2, 5 | eqnetrd 3008 |
. . . . . . . 8
⊢ (𝑝 = {𝑎, 𝑏} → 𝑝 ≠ ∅) |
| 7 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑝 = {𝑎, 𝑏} → 𝑝 ≠ ∅)) |
| 8 | 7 | rexlimivv 3201 |
. . . . . 6
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏} → 𝑝 ≠ ∅) |
| 9 | 8 | adantl 481 |
. . . . 5
⊢ ((𝑝 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}) → 𝑝 ≠ ∅) |
| 10 | 9 | pm4.71ri 560 |
. . . 4
⊢ ((𝑝 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}) ↔ (𝑝 ≠ ∅ ∧ (𝑝 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}))) |
| 11 | | ancom 460 |
. . . . . 6
⊢ ((𝑝 ≠ ∅ ∧ 𝑝 ∈ 𝒫 𝑉) ↔ (𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅)) |
| 12 | 11 | anbi1i 624 |
. . . . 5
⊢ (((𝑝 ≠ ∅ ∧ 𝑝 ∈ 𝒫 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}) ↔ ((𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏})) |
| 13 | | anass 468 |
. . . . 5
⊢ (((𝑝 ≠ ∅ ∧ 𝑝 ∈ 𝒫 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}) ↔ (𝑝 ≠ ∅ ∧ (𝑝 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}))) |
| 14 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ↔
(𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅)) |
| 15 | 14 | bicomi 224 |
. . . . . 6
⊢ ((𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅) ↔ 𝑝 ∈ (𝒫 𝑉 ∖ {∅})) |
| 16 | 15 | anbi1i 624 |
. . . . 5
⊢ (((𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}) ↔ (𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏})) |
| 17 | 12, 13, 16 | 3bitr3i 301 |
. . . 4
⊢ ((𝑝 ≠ ∅ ∧ (𝑝 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏})) ↔ (𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏})) |
| 18 | 10, 17 | bitri 275 |
. . 3
⊢ ((𝑝 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}) ↔ (𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏})) |
| 19 | 18 | rabbia2 3439 |
. 2
⊢ {𝑝 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}} = {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}} |
| 20 | 1, 19 | eqtrdi 2793 |
1
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}}) |