Step | Hyp | Ref
| Expression |
1 | | dnnumch.f |
. . . . 5
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) |
2 | | dnnumch.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | dnnumch.g |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) |
4 | 1, 2, 3 | dnnumch3 40467 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On) |
5 | | f1f1orn 6632 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))) |
7 | | f1f 6575 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On) |
8 | | frn 6512 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On → ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) ⊆ On) |
9 | 4, 7, 8 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) ⊆ On) |
10 | | epweon 7519 |
. . . 4
⊢ E We
On |
11 | | wess 5513 |
. . . 4
⊢ (ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) ⊆ On → ( E We On → E We
ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})))) |
12 | 9, 10, 11 | mpisyl 21 |
. . 3
⊢ (𝜑 → E We ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))) |
13 | | eqid 2739 |
. . . 4
⊢
{〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} = {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} |
14 | 13 | f1owe 7122 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) → ( E We ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) → {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴)) |
15 | 6, 12, 14 | sylc 65 |
. 2
⊢ (𝜑 → {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴) |
16 | | fvex 6690 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ∈ V |
17 | 16 | epeli 5437 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) ∈ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)) |
18 | 1, 2, 3 | dnnumch3lem 40466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
19 | 18 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
20 | 1, 2, 3 | dnnumch3lem 40466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
21 | 20 | adantrl 716 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
22 | 19, 21 | eleq12d 2828 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) ∈ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))) |
23 | 17, 22 | bitr2id 287 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}) ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))) |
24 | 23 | pm5.32da 582 |
. . . . . 6
⊢ (𝜑 → (((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})) ↔ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)))) |
25 | 24 | opabbidv 5097 |
. . . . 5
⊢ (𝜑 → {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))} = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))}) |
26 | | incom 4092 |
. . . . . 6
⊢ (𝐻 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝐻) |
27 | | df-xp 5532 |
. . . . . . 7
⊢ (𝐴 × 𝐴) = {〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} |
28 | | dnwech.h |
. . . . . . 7
⊢ 𝐻 = {〈𝑣, 𝑤〉 ∣ ∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})} |
29 | 27, 28 | ineq12i 4102 |
. . . . . 6
⊢ ((𝐴 × 𝐴) ∩ 𝐻) = ({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})}) |
30 | | inopab 5674 |
. . . . . 6
⊢
({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})}) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))} |
31 | 26, 29, 30 | 3eqtri 2766 |
. . . . 5
⊢ (𝐻 ∩ (𝐴 × 𝐴)) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))} |
32 | | incom 4092 |
. . . . . 6
⊢
({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) |
33 | 27 | ineq1i 4100 |
. . . . . 6
⊢ ((𝐴 × 𝐴) ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) = ({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) |
34 | | inopab 5674 |
. . . . . 6
⊢
({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))} |
35 | 32, 33, 34 | 3eqtri 2766 |
. . . . 5
⊢
({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))} |
36 | 25, 31, 35 | 3eqtr4g 2799 |
. . . 4
⊢ (𝜑 → (𝐻 ∩ (𝐴 × 𝐴)) = ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴))) |
37 | | weeq1 5514 |
. . . 4
⊢ ((𝐻 ∩ (𝐴 × 𝐴)) = ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) → ((𝐻 ∩ (𝐴 × 𝐴)) We 𝐴 ↔ ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) We 𝐴)) |
38 | 36, 37 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐻 ∩ (𝐴 × 𝐴)) We 𝐴 ↔ ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) We 𝐴)) |
39 | | weinxp 5608 |
. . 3
⊢ (𝐻 We 𝐴 ↔ (𝐻 ∩ (𝐴 × 𝐴)) We 𝐴) |
40 | | weinxp 5608 |
. . 3
⊢
({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴 ↔ ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) We 𝐴) |
41 | 38, 39, 40 | 3bitr4g 317 |
. 2
⊢ (𝜑 → (𝐻 We 𝐴 ↔ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴)) |
42 | 15, 41 | mpbird 260 |
1
⊢ (𝜑 → 𝐻 We 𝐴) |