Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
2 | | rfovd.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵 |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵) |
5 | 2, 4 | sselpwd 4734 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵) |
7 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
8 | 6, 7 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵) |
9 | | pwexg 4776 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑊 → 𝒫 𝐵 ∈ V) |
10 | 2, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝐵 ∈ V) |
11 | | rfovd.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
12 | 10, 11 | elmapd 7758 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)) |
13 | 8, 12 | mpbird 246 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑𝑚 𝐴)) |
14 | 13 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ (𝒫 𝐵 ↑𝑚 𝐴)) |
15 | | xpexg 6858 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
16 | 11, 2, 15 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
17 | 16 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝐴 × 𝐵) ∈ V) |
18 | 10, 11 | elmapd 7758 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵)) |
19 | 18 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → 𝑓:𝐴⟶𝒫 𝐵) |
20 | 19 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵) |
21 | 20 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝒫 𝐵)) |
22 | | elpwi 4117 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑓‘𝑥) ⊆ 𝐵) |
23 | 22 | sseld 3567 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥) ∈ 𝒫 𝐵 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)) |
24 | 21, 23 | syl6 34 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵))) |
25 | 24 | imdistand 724 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
26 | | a1tru 1491 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ⊤) |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ⊤)) |
28 | 25, 27 | jcad 554 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤))) |
29 | 28 | ssopab2dv 4929 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)}) |
30 | | opabssxp 5116 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⊤)} ⊆ (𝐴 × 𝐵) |
31 | 29, 30 | syl6ss 3580 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ (𝐴 × 𝐵)) |
32 | 17, 31 | sselpwd 4734 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ 𝒫 (𝐴 × 𝐵)) |
33 | | simplrr 797 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) |
34 | | elmapfn 7766 |
. . . . . 6
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → 𝑓 Fn 𝐴) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 Fn 𝐴) |
36 | 2 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝐵 ∈ 𝑊) |
37 | | rabexg 4739 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑊 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) |
38 | 37 | ralrimivw 2950 |
. . . . . 6
⊢ (𝐵 ∈ 𝑊 → ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) |
39 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
40 | 39 | fnmptf 5929 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴) |
41 | 36, 38, 40 | 3syl 18 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) Fn 𝐴) |
42 | | dfin5 3548 |
. . . . . . 7
⊢ (𝐵 ∩ (𝑓‘𝑢)) = {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} |
43 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) |
44 | 43 | simprd 478 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) |
45 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
46 | 44, 45 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
47 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴) |
48 | 46, 47 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ∈ 𝒫 𝐵) |
49 | 48 | elpwid 4118 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) ⊆ 𝐵) |
50 | | sseqin2 3779 |
. . . . . . . 8
⊢ ((𝑓‘𝑢) ⊆ 𝐵 ↔ (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢)) |
51 | 49, 50 | sylib 207 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝐵 ∩ (𝑓‘𝑢)) = (𝑓‘𝑢)) |
52 | | ibar 524 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐴 → (𝑏 ∈ (𝑓‘𝑢) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢)))) |
53 | 52 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑢 ∈ 𝐴 → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))}) |
54 | 53 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑏 ∈ (𝑓‘𝑢)} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))}) |
55 | 42, 51, 54 | 3eqtr3a 2668 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))}) |
56 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → (𝑥𝑟𝑦 ↔ 𝑥𝑟𝑏)) |
57 | 56 | cbvrabv 3172 |
. . . . . . . . . 10
⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏} |
58 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ 𝑎𝑟𝑏)) |
59 | | df-br 4584 |
. . . . . . . . . . . 12
⊢ (𝑎𝑟𝑏 ↔ 〈𝑎, 𝑏〉 ∈ 𝑟) |
60 | 58, 59 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑏 ↔ 〈𝑎, 𝑏〉 ∈ 𝑟)) |
61 | 60 | rabbidv 3164 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → {𝑏 ∈ 𝐵 ∣ 𝑥𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 〈𝑎, 𝑏〉 ∈ 𝑟}) |
62 | 57, 61 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 〈𝑎, 𝑏〉 ∈ 𝑟}) |
63 | 62 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 〈𝑎, 𝑏〉 ∈ 𝑟}) |
64 | 63 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 〈𝑎, 𝑏〉 ∈ 𝑟})) |
65 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑎 = 𝑢) |
66 | 65 | opeq1d 4346 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 〈𝑎, 𝑏〉 = 〈𝑢, 𝑏〉) |
67 | | simpllr 795 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
68 | 66, 67 | eleq12d 2682 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (〈𝑎, 𝑏〉 ∈ 𝑟 ↔ 〈𝑢, 𝑏〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) |
69 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
70 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
71 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑥 = 𝑢) |
72 | 71 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴)) |
73 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → 𝑦 = 𝑏) |
74 | 71 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑓‘𝑥) = (𝑓‘𝑢)) |
75 | 73, 74 | eleq12d 2682 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑏 ∈ (𝑓‘𝑢))) |
76 | 72, 75 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑏) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢)))) |
77 | 69, 70, 76 | opelopaba 4916 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑏〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))) |
78 | 68, 77 | syl6bb 275 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → (〈𝑎, 𝑏〉 ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢)))) |
79 | 78 | rabbidv 3164 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ 〈𝑎, 𝑏〉 ∈ 𝑟} = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))}) |
80 | 2 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
81 | | rabexg 4739 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V) |
82 | 80, 81 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))} ∈ V) |
83 | 64, 79, 47, 82 | fvmptd 6197 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢) = {𝑏 ∈ 𝐵 ∣ (𝑢 ∈ 𝐴 ∧ 𝑏 ∈ (𝑓‘𝑢))}) |
84 | 55, 83 | eqtr4d 2647 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑢)) |
85 | 35, 41, 84 | eqfnfvd 6222 |
. . . 4
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
86 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) |
87 | 86 | elpwid 4118 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵)) |
88 | | xpss 5149 |
. . . . . . 7
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
89 | 87, 88 | syl6ss 3580 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V)) |
90 | | df-rel 5045 |
. . . . . 6
⊢ (Rel
𝑟 ↔ 𝑟 ⊆ (V × V)) |
91 | 89, 90 | sylibr 223 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟) |
92 | | relopab 5169 |
. . . . . 6
⊢ Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} |
93 | 92 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
94 | | simpl 472 |
. . . . . . 7
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) |
95 | 2, 94 | anim12i 588 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) → (𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵))) |
96 | 95 | anim1i 590 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
97 | | vex 3176 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
98 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢) |
99 | 98 | eleq1d 2672 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴)) |
100 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣) |
101 | 98 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑓‘𝑥) = (𝑓‘𝑢)) |
102 | 100, 101 | eleq12d 2682 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑣 ∈ (𝑓‘𝑢))) |
103 | 99, 102 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)))) |
104 | 69, 97, 103 | opelopaba 4916 |
. . . . . . 7
⊢
(〈𝑢, 𝑣〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢))) |
105 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ 𝑢𝑟𝑣)) |
106 | | df-br 4584 |
. . . . . . . . . . . 12
⊢ (𝑢𝑟𝑣 ↔ 〈𝑢, 𝑣〉 ∈ 𝑟) |
107 | 105, 106 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑣 → (𝑢𝑟𝑏 ↔ 〈𝑢, 𝑣〉 ∈ 𝑟)) |
108 | 107 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ↔ (𝑣 ∈ 𝐵 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟)) |
109 | 108 | anbi2i 726 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟))) |
110 | 109 | a1i 11 |
. . . . . . . 8
⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟)))) |
111 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
112 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝑥𝑟𝑦 ↔ 𝑎𝑟𝑦)) |
113 | 112 | rabbidv 3164 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦}) |
114 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑏 → (𝑎𝑟𝑦 ↔ 𝑎𝑟𝑏)) |
115 | 114 | cbvrabv 3172 |
. . . . . . . . . . . . . 14
⊢ {𝑦 ∈ 𝐵 ∣ 𝑎𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} |
116 | 113, 115 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}) |
117 | 116 | cbvmptv 4678 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏}) |
118 | 111, 117 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑓 = (𝑎 ∈ 𝐴 ↦ {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏})) |
119 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑢 → (𝑎𝑟𝑏 ↔ 𝑢𝑟𝑏)) |
120 | 119 | rabbidv 3164 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑢 → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) |
121 | 120 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) ∧ 𝑎 = 𝑢) → {𝑏 ∈ 𝐵 ∣ 𝑎𝑟𝑏} = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) |
122 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴) |
123 | | rabexg 4739 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑊 → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V) |
124 | 123 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏} ∈ V) |
125 | 118, 121,
122, 124 | fvmptd 6197 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑓‘𝑢) = {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}) |
126 | 125 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ (𝑓‘𝑢) ↔ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏})) |
127 | 126 | pm5.32da 671 |
. . . . . . . 8
⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐵 ∣ 𝑢𝑟𝑏}))) |
128 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) |
129 | 128 | elpwid 4118 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵)) |
130 | 69, 97 | opeldm 5250 |
. . . . . . . . . . . 12
⊢
(〈𝑢, 𝑣〉 ∈ 𝑟 → 𝑢 ∈ dom 𝑟) |
131 | | dmss 5245 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ dom (𝐴 × 𝐵)) |
132 | | dmxpss 5484 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐴 × 𝐵) ⊆ 𝐴 |
133 | 131, 132 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → dom 𝑟 ⊆ 𝐴) |
134 | 133 | sseld 3567 |
. . . . . . . . . . . 12
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑢 ∈ dom 𝑟 → 𝑢 ∈ 𝐴)) |
135 | 130, 134 | syl5 33 |
. . . . . . . . . . 11
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (〈𝑢, 𝑣〉 ∈ 𝑟 → 𝑢 ∈ 𝐴)) |
136 | 135 | pm4.71rd 665 |
. . . . . . . . . 10
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (〈𝑢, 𝑣〉 ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟))) |
137 | 69, 97 | opelrn 5278 |
. . . . . . . . . . . . 13
⊢
(〈𝑢, 𝑣〉 ∈ 𝑟 → 𝑣 ∈ ran 𝑟) |
138 | | rnss 5275 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ ran (𝐴 × 𝐵)) |
139 | | rnxpss 5485 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
140 | 138, 139 | syl6ss 3580 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ran 𝑟 ⊆ 𝐵) |
141 | 140 | sseld 3567 |
. . . . . . . . . . . . 13
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (𝑣 ∈ ran 𝑟 → 𝑣 ∈ 𝐵)) |
142 | 137, 141 | syl5 33 |
. . . . . . . . . . . 12
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (〈𝑢, 𝑣〉 ∈ 𝑟 → 𝑣 ∈ 𝐵)) |
143 | 142 | pm4.71rd 665 |
. . . . . . . . . . 11
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (〈𝑢, 𝑣〉 ∈ 𝑟 ↔ (𝑣 ∈ 𝐵 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟))) |
144 | 143 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → ((𝑢 ∈ 𝐴 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟) ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟)))) |
145 | 136, 144 | bitrd 267 |
. . . . . . . . 9
⊢ (𝑟 ⊆ (𝐴 × 𝐵) → (〈𝑢, 𝑣〉 ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟)))) |
146 | 129, 145 | syl 17 |
. . . . . . . 8
⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (〈𝑢, 𝑣〉 ∈ 𝑟 ↔ (𝑢 ∈ 𝐴 ∧ (𝑣 ∈ 𝐵 ∧ 〈𝑢, 𝑣〉 ∈ 𝑟)))) |
147 | 110, 127,
146 | 3bitr4d 299 |
. . . . . . 7
⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ (𝑓‘𝑢)) ↔ 〈𝑢, 𝑣〉 ∈ 𝑟)) |
148 | 104, 147 | syl5rbb 272 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (〈𝑢, 𝑣〉 ∈ 𝑟 ↔ 〈𝑢, 𝑣〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) |
149 | 148 | eqrelrdv2 5142 |
. . . . 5
⊢ (((Rel
𝑟 ∧ Rel {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ ((𝐵 ∈ 𝑊 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
150 | 91, 93, 96, 149 | syl21anc 1317 |
. . . 4
⊢ (((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
151 | 85, 150 | impbida 873 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴))) → (𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
152 | 1, 14, 32, 151 | f1ocnv2d 6784 |
. 2
⊢ (𝜑 → ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))) |
153 | | rfovcnvf1od.f |
. . . 4
⊢ 𝐹 = (𝐴𝑂𝐵) |
154 | | rfovd.rf |
. . . . 5
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦}))) |
155 | 154, 11, 2 | rfovd 37315 |
. . . 4
⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
156 | 153, 155 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
157 | | f1oeq1 6040 |
. . . 4
⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴))) |
158 | | cnveq 5218 |
. . . . 5
⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ◡𝐹 = ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
159 | 158 | eqeq1d 2612 |
. . . 4
⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))) |
160 | 157, 159 | anbi12d 743 |
. . 3
⊢ (𝐹 = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))) |
161 | 156, 160 | syl 17 |
. 2
⊢ (𝜑 → ((𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) ↔ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})):𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴) ∧ ◡(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))) |
162 | 152, 161 | mpbird 246 |
1
⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))) |