Proof of Theorem fpwwecbv
Step | Hyp | Ref
| Expression |
1 | | fpwwe.1 |
. 2
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
2 | | simpl 482 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → 𝑥 = 𝑎) |
3 | 2 | sseq1d 3954 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴)) |
4 | | simpr 484 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → 𝑟 = 𝑠) |
5 | 2 | sqxpeqd 5623 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑥 × 𝑥) = (𝑎 × 𝑎)) |
6 | 4, 5 | sseq12d 3956 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑠 ⊆ (𝑎 × 𝑎))) |
7 | 3, 6 | anbi12d 630 |
. . . 4
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)))) |
8 | | weeq2 5580 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑎)) |
9 | | weeq1 5579 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (𝑟 We 𝑎 ↔ 𝑠 We 𝑎)) |
10 | 8, 9 | sylan9bb 509 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑟 We 𝑥 ↔ 𝑠 We 𝑎)) |
11 | | sneq 4574 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
12 | 11 | imaeq2d 5970 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (◡𝑟 “ {𝑦}) = (◡𝑟 “ {𝑧})) |
13 | 12 | fveq2d 6796 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐹‘(◡𝑟 “ {𝑦})) = (𝐹‘(◡𝑟 “ {𝑧}))) |
14 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
15 | 13, 14 | eqeq12d 2749 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝐹‘(◡𝑟 “ {𝑦})) = 𝑦 ↔ (𝐹‘(◡𝑟 “ {𝑧})) = 𝑧)) |
16 | 15 | cbvralvw 3385 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦 ↔ ∀𝑧 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑧})) = 𝑧) |
17 | 4 | cnveqd 5788 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ◡𝑟 = ◡𝑠) |
18 | 17 | imaeq1d 5969 |
. . . . . . . 8
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (◡𝑟 “ {𝑧}) = (◡𝑠 “ {𝑧})) |
19 | 18 | fveqeq2d 6800 |
. . . . . . 7
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ((𝐹‘(◡𝑟 “ {𝑧})) = 𝑧 ↔ (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧)) |
20 | 2, 19 | raleqbidv 3338 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (∀𝑧 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑧})) = 𝑧 ↔ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧)) |
21 | 16, 20 | bitrid 282 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦 ↔ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧)) |
22 | 10, 21 | anbi12d 630 |
. . . 4
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ((𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦) ↔ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))) |
23 | 7, 22 | anbi12d 630 |
. . 3
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦)) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧)))) |
24 | 23 | cbvopabv 5150 |
. 2
⊢
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))} |
25 | 1, 24 | eqtri 2761 |
1
⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))} |