| Step | Hyp | Ref
| Expression |
| 1 | | dnnumch.f |
. . . . 5
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) |
| 2 | | dnnumch.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 3 | | dnnumch.g |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) |
| 4 | 1, 2, 3 | dnnumch3 43059 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On) |
| 5 | | f1f1orn 6859 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))) |
| 6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))) |
| 7 | | f1f 6804 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On) |
| 8 | | frn 6743 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On → ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) ⊆ On) |
| 9 | 4, 7, 8 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) ⊆ On) |
| 10 | | epweon 7795 |
. . . 4
⊢ E We
On |
| 11 | | wess 5671 |
. . . 4
⊢ (ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) ⊆ On → ( E We On → E We
ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})))) |
| 12 | 9, 10, 11 | mpisyl 21 |
. . 3
⊢ (𝜑 → E We ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))) |
| 13 | | eqid 2737 |
. . . 4
⊢
{〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} = {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} |
| 14 | 13 | f1owe 7373 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1-onto→ran
(𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) → ( E We ran (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) → {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴)) |
| 15 | 6, 12, 14 | sylc 65 |
. 2
⊢ (𝜑 → {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴) |
| 16 | | fvex 6919 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ∈ V |
| 17 | 16 | epeli 5586 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) ∈ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)) |
| 18 | 1, 2, 3 | dnnumch3lem 43058 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
| 19 | 18 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
| 20 | 1, 2, 3 | dnnumch3lem 43058 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
| 21 | 20 | adantrl 716 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
| 22 | 19, 21 | eleq12d 2835 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) ∈ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))) |
| 23 | 17, 22 | bitr2id 284 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}) ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))) |
| 24 | 23 | pm5.32da 579 |
. . . . . 6
⊢ (𝜑 → (((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})) ↔ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)))) |
| 25 | 24 | opabbidv 5209 |
. . . . 5
⊢ (𝜑 → {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))} = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))}) |
| 26 | | incom 4209 |
. . . . . 6
⊢ (𝐻 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝐻) |
| 27 | | df-xp 5691 |
. . . . . . 7
⊢ (𝐴 × 𝐴) = {〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} |
| 28 | | dnwech.h |
. . . . . . 7
⊢ 𝐻 = {〈𝑣, 𝑤〉 ∣ ∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})} |
| 29 | 27, 28 | ineq12i 4218 |
. . . . . 6
⊢ ((𝐴 × 𝐴) ∩ 𝐻) = ({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})}) |
| 30 | | inopab 5839 |
. . . . . 6
⊢
({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ∩
(◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})}) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))} |
| 31 | 26, 29, 30 | 3eqtri 2769 |
. . . . 5
⊢ (𝐻 ∩ (𝐴 × 𝐴)) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤}))} |
| 32 | | incom 4209 |
. . . . . 6
⊢
({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) |
| 33 | 27 | ineq1i 4216 |
. . . . . 6
⊢ ((𝐴 × 𝐴) ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) = ({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) |
| 34 | | inopab 5839 |
. . . . . 6
⊢
({〈𝑣, 𝑤〉 ∣ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)} ∩ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)}) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))} |
| 35 | 32, 33, 34 | 3eqtri 2769 |
. . . . 5
⊢
({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) = {〈𝑣, 𝑤〉 ∣ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤))} |
| 36 | 25, 31, 35 | 3eqtr4g 2802 |
. . . 4
⊢ (𝜑 → (𝐻 ∩ (𝐴 × 𝐴)) = ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴))) |
| 37 | | weeq1 5672 |
. . . 4
⊢ ((𝐻 ∩ (𝐴 × 𝐴)) = ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) → ((𝐻 ∩ (𝐴 × 𝐴)) We 𝐴 ↔ ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) We 𝐴)) |
| 38 | 36, 37 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐻 ∩ (𝐴 × 𝐴)) We 𝐴 ↔ ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) We 𝐴)) |
| 39 | | weinxp 5770 |
. . 3
⊢ (𝐻 We 𝐴 ↔ (𝐻 ∩ (𝐴 × 𝐴)) We 𝐴) |
| 40 | | weinxp 5770 |
. . 3
⊢
({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴 ↔ ({〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} ∩ (𝐴 × 𝐴)) We 𝐴) |
| 41 | 38, 39, 40 | 3bitr4g 314 |
. 2
⊢ (𝜑 → (𝐻 We 𝐴 ↔ {〈𝑣, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) E ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤)} We 𝐴)) |
| 42 | 15, 41 | mpbird 257 |
1
⊢ (𝜑 → 𝐻 We 𝐴) |