Step | Hyp | Ref
| Expression |
1 | | df-ov 7186 |
. . . . . 6
⊢ (𝑌(𝐹 ∘ 1st )𝑅) = ((𝐹 ∘ 1st )‘〈𝑌, 𝑅〉) |
2 | | fo1st 7747 |
. . . . . . . 8
⊢
1st :V–onto→V |
3 | | fofn 6605 |
. . . . . . . 8
⊢
(1st :V–onto→V → 1st Fn V) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
⊢
1st Fn V |
5 | | opex 5332 |
. . . . . . 7
⊢
〈𝑌, 𝑅〉 ∈ V |
6 | | fvco2 6778 |
. . . . . . 7
⊢
((1st Fn V ∧ 〈𝑌, 𝑅〉 ∈ V) → ((𝐹 ∘ 1st )‘〈𝑌, 𝑅〉) = (𝐹‘(1st ‘〈𝑌, 𝑅〉))) |
7 | 4, 5, 6 | mp2an 692 |
. . . . . 6
⊢ ((𝐹 ∘ 1st
)‘〈𝑌, 𝑅〉) = (𝐹‘(1st ‘〈𝑌, 𝑅〉)) |
8 | 1, 7 | eqtri 2762 |
. . . . 5
⊢ (𝑌(𝐹 ∘ 1st )𝑅) = (𝐹‘(1st ‘〈𝑌, 𝑅〉)) |
9 | | fpwwe.1 |
. . . . . . . 8
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
10 | 9 | bropaex12 5623 |
. . . . . . 7
⊢ (𝑌𝑊𝑅 → (𝑌 ∈ V ∧ 𝑅 ∈ V)) |
11 | | op1stg 7739 |
. . . . . . 7
⊢ ((𝑌 ∈ V ∧ 𝑅 ∈ V) →
(1st ‘〈𝑌, 𝑅〉) = 𝑌) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝑌𝑊𝑅 → (1st ‘〈𝑌, 𝑅〉) = 𝑌) |
13 | 12 | fveq2d 6691 |
. . . . 5
⊢ (𝑌𝑊𝑅 → (𝐹‘(1st ‘〈𝑌, 𝑅〉)) = (𝐹‘𝑌)) |
14 | 8, 13 | syl5eq 2786 |
. . . 4
⊢ (𝑌𝑊𝑅 → (𝑌(𝐹 ∘ 1st )𝑅) = (𝐹‘𝑌)) |
15 | 14 | eleq1d 2818 |
. . 3
⊢ (𝑌𝑊𝑅 → ((𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌 ↔ (𝐹‘𝑌) ∈ 𝑌)) |
16 | 15 | pm5.32i 578 |
. 2
⊢ ((𝑌𝑊𝑅 ∧ (𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌) ↔ (𝑌𝑊𝑅 ∧ (𝐹‘𝑌) ∈ 𝑌)) |
17 | | vex 3404 |
. . . . . . . . . . 11
⊢ 𝑟 ∈ V |
18 | 17 | cnvex 7669 |
. . . . . . . . . 10
⊢ ◡𝑟 ∈ V |
19 | 18 | imaex 7660 |
. . . . . . . . 9
⊢ (◡𝑟 “ {𝑦}) ∈ V |
20 | | vex 3404 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
21 | 17 | inex1 5195 |
. . . . . . . . . . . 12
⊢ (𝑟 ∩ (𝑢 × 𝑢)) ∈ V |
22 | 20, 21 | algrflem 7858 |
. . . . . . . . . . 11
⊢ (𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = (𝐹‘𝑢) |
23 | | fveq2 6687 |
. . . . . . . . . . 11
⊢ (𝑢 = (◡𝑟 “ {𝑦}) → (𝐹‘𝑢) = (𝐹‘(◡𝑟 “ {𝑦}))) |
24 | 22, 23 | syl5eq 2786 |
. . . . . . . . . 10
⊢ (𝑢 = (◡𝑟 “ {𝑦}) → (𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = (𝐹‘(◡𝑟 “ {𝑦}))) |
25 | 24 | eqeq1d 2741 |
. . . . . . . . 9
⊢ (𝑢 = (◡𝑟 “ {𝑦}) → ((𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦)) |
26 | 19, 25 | sbcie 3728 |
. . . . . . . 8
⊢
([(◡𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦) |
27 | 26 | ralbii 3081 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦) |
28 | 27 | anbi2i 626 |
. . . . . 6
⊢ ((𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦) ↔ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦)) |
29 | 28 | anbi2i 626 |
. . . . 5
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦)) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))) |
30 | 29 | opabbii 5107 |
. . . 4
⊢
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
31 | 9, 30 | eqtr4i 2765 |
. . 3
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
32 | | fpwwe.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
33 | | vex 3404 |
. . . . 5
⊢ 𝑥 ∈ V |
34 | 33, 17 | algrflem 7858 |
. . . 4
⊢ (𝑥(𝐹 ∘ 1st )𝑟) = (𝐹‘𝑥) |
35 | | simp1 1137 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ⊆ 𝐴) |
36 | | velpw 4503 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
37 | 35, 36 | sylibr 237 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴) |
38 | | 19.8a 2182 |
. . . . . . . 8
⊢ (𝑟 We 𝑥 → ∃𝑟 𝑟 We 𝑥) |
39 | 38 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → ∃𝑟 𝑟 We 𝑥) |
40 | | ween 9548 |
. . . . . . 7
⊢ (𝑥 ∈ dom card ↔
∃𝑟 𝑟 We 𝑥) |
41 | 39, 40 | sylibr 237 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ dom card) |
42 | 37, 41 | elind 4094 |
. . . . 5
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) |
43 | | fpwwe.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) |
44 | 42, 43 | sylan2 596 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝐹‘𝑥) ∈ 𝐴) |
45 | 34, 44 | eqeltrid 2838 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥(𝐹 ∘ 1st )𝑟) ∈ 𝐴) |
46 | | fpwwe.4 |
. . 3
⊢ 𝑋 = ∪
dom 𝑊 |
47 | 31, 32, 45, 46 | fpwwe2 10156 |
. 2
⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))) |
48 | 16, 47 | bitr3id 288 |
1
⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝐹‘𝑌) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))) |