Step | Hyp | Ref
| Expression |
1 | | fpwwe2.1 |
. 2
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
2 | | simpl 483 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → 𝑥 = 𝑎) |
3 | 2 | sseq1d 3975 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴)) |
4 | | simpr 485 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → 𝑟 = 𝑠) |
5 | 2 | sqxpeqd 5665 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑥 × 𝑥) = (𝑎 × 𝑎)) |
6 | 4, 5 | sseq12d 3977 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑠 ⊆ (𝑎 × 𝑎))) |
7 | 3, 6 | anbi12d 631 |
. . . 4
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)))) |
8 | | weeq2 5622 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑎)) |
9 | | weeq1 5621 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (𝑟 We 𝑎 ↔ 𝑠 We 𝑎)) |
10 | 8, 9 | sylan9bb 510 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑟 We 𝑥 ↔ 𝑠 We 𝑎)) |
11 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → 𝑢 = 𝑣) |
12 | 11 | sqxpeqd 5665 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝑢 × 𝑢) = (𝑣 × 𝑣)) |
13 | 12 | ineq2d 4172 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → (𝑟 ∩ (𝑢 × 𝑢)) = (𝑟 ∩ (𝑣 × 𝑣))) |
14 | 11, 13 | oveq12d 7375 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑣 → (𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣)))) |
15 | 14 | eqeq1d 2738 |
. . . . . . . . 9
⊢ (𝑢 = 𝑣 → ((𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦)) |
16 | 15 | cbvsbcvw 3774 |
. . . . . . . 8
⊢
([(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ [(◡𝑟 “ {𝑦}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦) |
17 | | sneq 4596 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
18 | 17 | imaeq2d 6013 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (◡𝑟 “ {𝑦}) = (◡𝑟 “ {𝑧})) |
19 | | eqeq2 2748 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦 ↔ (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧)) |
20 | 18, 19 | sbceqbid 3746 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ([(◡𝑟 “ {𝑦}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦 ↔ [(◡𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧)) |
21 | 16, 20 | bitrid 282 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ([(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ [(◡𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧)) |
22 | 21 | cbvralvw 3225 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑧 ∈ 𝑥 [(◡𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧) |
23 | 4 | cnveqd 5831 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ◡𝑟 = ◡𝑠) |
24 | 23 | imaeq1d 6012 |
. . . . . . . 8
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (◡𝑟 “ {𝑧}) = (◡𝑠 “ {𝑧})) |
25 | 4 | ineq1d 4171 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑟 ∩ (𝑣 × 𝑣)) = (𝑠 ∩ (𝑣 × 𝑣))) |
26 | 25 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = (𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣)))) |
27 | 26 | eqeq1d 2738 |
. . . . . . . 8
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ((𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧 ↔ (𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧)) |
28 | 24, 27 | sbceqbid 3746 |
. . . . . . 7
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ([(◡𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧 ↔ [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧)) |
29 | 2, 28 | raleqbidv 3319 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (∀𝑧 ∈ 𝑥 [(◡𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧 ↔ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧)) |
30 | 22, 29 | bitrid 282 |
. . . . 5
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧)) |
31 | 10, 30 | anbi12d 631 |
. . . 4
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → ((𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦) ↔ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))) |
32 | 7, 31 | anbi12d 631 |
. . 3
⊢ ((𝑥 = 𝑎 ∧ 𝑟 = 𝑠) → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦)) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧)))) |
33 | 32 | cbvopabv 5178 |
. 2
⊢
{⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} |
34 | 1, 33 | eqtri 2764 |
1
⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} |