Step | Hyp | Ref
| Expression |
1 | | fpwwe2.1 |
. . . . . 6
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} |
2 | 1 | relopabiv 5780 |
. . . . 5
β’ Rel π |
3 | 2 | a1i 11 |
. . . 4
β’ (π β Rel π) |
4 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π = (π‘ β© (π€ Γ π€)))) β π = (π‘ β© (π€ Γ π€))) |
5 | | fpwwe2.2 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β π) |
6 | 1, 5 | fpwwe2lem2 10576 |
. . . . . . . . . . . . . 14
β’ (π β (π€ππ‘ β ((π€ β π΄ β§ π‘ β (π€ Γ π€)) β§ (π‘ We π€ β§ βπ¦ β π€ [(β‘π‘ β {π¦}) / π’](π’πΉ(π‘ β© (π’ Γ π’))) = π¦)))) |
7 | 6 | simprbda 500 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ππ‘) β (π€ β π΄ β§ π‘ β (π€ Γ π€))) |
8 | 7 | simprd 497 |
. . . . . . . . . . . 12
β’ ((π β§ π€ππ‘) β π‘ β (π€ Γ π€)) |
9 | 8 | adantrl 715 |
. . . . . . . . . . 11
β’ ((π β§ (π€ππ β§ π€ππ‘)) β π‘ β (π€ Γ π€)) |
10 | 9 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π = (π‘ β© (π€ Γ π€)))) β π‘ β (π€ Γ π€)) |
11 | | df-ss 3931 |
. . . . . . . . . 10
β’ (π‘ β (π€ Γ π€) β (π‘ β© (π€ Γ π€)) = π‘) |
12 | 10, 11 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π = (π‘ β© (π€ Γ π€)))) β (π‘ β© (π€ Γ π€)) = π‘) |
13 | 4, 12 | eqtrd 2773 |
. . . . . . . 8
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π = (π‘ β© (π€ Γ π€)))) β π = π‘) |
14 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π‘ = (π β© (π€ Γ π€)))) β π‘ = (π β© (π€ Γ π€))) |
15 | 1, 5 | fpwwe2lem2 10576 |
. . . . . . . . . . . . . 14
β’ (π β (π€ππ β ((π€ β π΄ β§ π β (π€ Γ π€)) β§ (π We π€ β§ βπ¦ β π€ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦)))) |
16 | 15 | simprbda 500 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ππ ) β (π€ β π΄ β§ π β (π€ Γ π€))) |
17 | 16 | simprd 497 |
. . . . . . . . . . . 12
β’ ((π β§ π€ππ ) β π β (π€ Γ π€)) |
18 | 17 | adantrr 716 |
. . . . . . . . . . 11
β’ ((π β§ (π€ππ β§ π€ππ‘)) β π β (π€ Γ π€)) |
19 | 18 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π‘ = (π β© (π€ Γ π€)))) β π β (π€ Γ π€)) |
20 | | df-ss 3931 |
. . . . . . . . . 10
β’ (π β (π€ Γ π€) β (π β© (π€ Γ π€)) = π ) |
21 | 19, 20 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π‘ = (π β© (π€ Γ π€)))) β (π β© (π€ Γ π€)) = π ) |
22 | 14, 21 | eqtr2d 2774 |
. . . . . . . 8
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π€ β π€ β§ π‘ = (π β© (π€ Γ π€)))) β π = π‘) |
23 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π€ππ β§ π€ππ‘)) β π΄ β π) |
24 | | fpwwe2.3 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) |
25 | 24 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ (π€ππ β§ π€ππ‘)) β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) |
26 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π€ππ β§ π€ππ‘)) β π€ππ ) |
27 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π€ππ β§ π€ππ‘)) β π€ππ‘) |
28 | 1, 23, 25, 26, 27 | fpwwe2lem9 10583 |
. . . . . . . 8
β’ ((π β§ (π€ππ β§ π€ππ‘)) β ((π€ β π€ β§ π = (π‘ β© (π€ Γ π€))) β¨ (π€ β π€ β§ π‘ = (π β© (π€ Γ π€))))) |
29 | 13, 22, 28 | mpjaodan 958 |
. . . . . . 7
β’ ((π β§ (π€ππ β§ π€ππ‘)) β π = π‘) |
30 | 29 | ex 414 |
. . . . . 6
β’ (π β ((π€ππ β§ π€ππ‘) β π = π‘)) |
31 | 30 | alrimiv 1931 |
. . . . 5
β’ (π β βπ‘((π€ππ β§ π€ππ‘) β π = π‘)) |
32 | 31 | alrimivv 1932 |
. . . 4
β’ (π β βπ€βπ βπ‘((π€ππ β§ π€ππ‘) β π = π‘)) |
33 | | dffun2 6510 |
. . . 4
β’ (Fun
π β (Rel π β§ βπ€βπ βπ‘((π€ππ β§ π€ππ‘) β π = π‘))) |
34 | 3, 32, 33 | sylanbrc 584 |
. . 3
β’ (π β Fun π) |
35 | 34 | funfnd 6536 |
. 2
β’ (π β π Fn dom π) |
36 | | vex 3451 |
. . . . 5
β’ π β V |
37 | 36 | elrn 5853 |
. . . 4
β’ (π β ran π β βπ€ π€ππ ) |
38 | 2 | releldmi 5907 |
. . . . . . . . . . . 12
β’ (π€ππ β π€ β dom π) |
39 | 38 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π€ππ ) β π€ β dom π) |
40 | | elssuni 4902 |
. . . . . . . . . . 11
β’ (π€ β dom π β π€ β βͺ dom
π) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π€ππ ) β π€ β βͺ dom
π) |
42 | | fpwwe2.4 |
. . . . . . . . . 10
β’ π = βͺ
dom π |
43 | 41, 42 | sseqtrrdi 3999 |
. . . . . . . . 9
β’ ((π β§ π€ππ ) β π€ β π) |
44 | | xpss12 5652 |
. . . . . . . . 9
β’ ((π€ β π β§ π€ β π) β (π€ Γ π€) β (π Γ π)) |
45 | 43, 43, 44 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π€ππ ) β (π€ Γ π€) β (π Γ π)) |
46 | 17, 45 | sstrd 3958 |
. . . . . . 7
β’ ((π β§ π€ππ ) β π β (π Γ π)) |
47 | 46 | ex 414 |
. . . . . 6
β’ (π β (π€ππ β π β (π Γ π))) |
48 | | velpw 4569 |
. . . . . 6
β’ (π β π« (π Γ π) β π β (π Γ π)) |
49 | 47, 48 | syl6ibr 252 |
. . . . 5
β’ (π β (π€ππ β π β π« (π Γ π))) |
50 | 49 | exlimdv 1937 |
. . . 4
β’ (π β (βπ€ π€ππ β π β π« (π Γ π))) |
51 | 37, 50 | biimtrid 241 |
. . 3
β’ (π β (π β ran π β π β π« (π Γ π))) |
52 | 51 | ssrdv 3954 |
. 2
β’ (π β ran π β π« (π Γ π)) |
53 | | df-f 6504 |
. 2
β’ (π:dom πβΆπ« (π Γ π) β (π Fn dom π β§ ran π β π« (π Γ π))) |
54 | 35, 52, 53 | sylanbrc 584 |
1
β’ (π β π:dom πβΆπ« (π Γ π)) |