Step | Hyp | Ref
| Expression |
1 | | fpwwe2.1 |
. . . . . . . . . . 11
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} |
2 | | fpwwe2.2 |
. . . . . . . . . . 11
β’ (π β π΄ β π) |
3 | | fpwwe2.3 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) |
4 | | fpwwe2.4 |
. . . . . . . . . . 11
β’ π = βͺ
dom π |
5 | 1, 2, 3, 4 | fpwwe2lem10 10583 |
. . . . . . . . . 10
β’ (π β π:dom πβΆπ« (π Γ π)) |
6 | 5 | ffund 6677 |
. . . . . . . . 9
β’ (π β Fun π) |
7 | | funbrfv2b 6905 |
. . . . . . . . 9
β’ (Fun
π β (πππ
β (π β dom π β§ (πβπ) = π
))) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (π β (πππ
β (π β dom π β§ (πβπ) = π
))) |
9 | 8 | simprbda 500 |
. . . . . . 7
β’ ((π β§ πππ
) β π β dom π) |
10 | 9 | adantrr 716 |
. . . . . 6
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β π β dom π) |
11 | | elssuni 4903 |
. . . . . . 7
β’ (π β dom π β π β βͺ dom
π) |
12 | 11, 4 | sseqtrrdi 4000 |
. . . . . 6
β’ (π β dom π β π β π) |
13 | 10, 12 | syl 17 |
. . . . 5
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β π β π) |
14 | | simpl 484 |
. . . . . . 7
β’ ((π β π β§ (πβπ) = (π
β© (π Γ π))) β π β π) |
15 | 14 | a1i 11 |
. . . . . 6
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β ((π β π β§ (πβπ) = (π
β© (π Γ π))) β π β π)) |
16 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (ππΉπ
) β π) |
17 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β π΄ β π) |
18 | 17 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β π΄ β π) |
19 | 1, 2, 3, 4 | fpwwe2lem11 10584 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β dom π) |
20 | | funfvbrb 7006 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Fun
π β (π β dom π β ππ(πβπ))) |
21 | 6, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β dom π β ππ(πβπ))) |
22 | 19, 21 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ππ(πβπ)) |
23 | 1, 2 | fpwwe2lem2 10575 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (ππ(πβπ) β ((π β π΄ β§ (πβπ) β (π Γ π)) β§ ((πβπ) We π β§ βπ¦ β π [(β‘(πβπ) β {π¦}) / π’](π’πΉ((πβπ) β© (π’ Γ π’))) = π¦)))) |
24 | 22, 23 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π β π΄ β§ (πβπ) β (π Γ π)) β§ ((πβπ) We π β§ βπ¦ β π [(β‘(πβπ) β {π¦}) / π’](π’πΉ((πβπ) β© (π’ Γ π’))) = π¦))) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β ((π β π΄ β§ (πβπ) β (π Γ π)) β§ ((πβπ) We π β§ βπ¦ β π [(β‘(πβπ) β {π¦}) / π’](π’πΉ((πβπ) β© (π’ Γ π’))) = π¦))) |
26 | 25 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (π β π΄ β§ (πβπ) β (π Γ π))) |
27 | 26 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β π β π΄) |
28 | 18, 27 | ssexd 5286 |
. . . . . . . . . . . . 13
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β π β V) |
29 | 28 | difexd 5291 |
. . . . . . . . . . . 12
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (π β π) β V) |
30 | 25 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β ((πβπ) We π β§ βπ¦ β π [(β‘(πβπ) β {π¦}) / π’](π’πΉ((πβπ) β© (π’ Γ π’))) = π¦)) |
31 | 30 | simpld 496 |
. . . . . . . . . . . . 13
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (πβπ) We π) |
32 | | wefr 5628 |
. . . . . . . . . . . . 13
β’ ((πβπ) We π β (πβπ) Fr π) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (πβπ) Fr π) |
34 | | difssd 4097 |
. . . . . . . . . . . 12
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (π β π) β π) |
35 | | fri 5598 |
. . . . . . . . . . . . 13
β’ ((((π β π) β V β§ (πβπ) Fr π) β§ ((π β π) β π β§ (π β π) β β
)) β βπ§ β (π β π)βπ€ β (π β π) Β¬ π€(πβπ)π§) |
36 | 35 | expr 458 |
. . . . . . . . . . . 12
β’ ((((π β π) β V β§ (πβπ) Fr π) β§ (π β π) β π) β ((π β π) β β
β βπ§ β (π β π)βπ€ β (π β π) Β¬ π€(πβπ)π§)) |
37 | 29, 33, 34, 36 | syl21anc 837 |
. . . . . . . . . . 11
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β ((π β π) β β
β βπ§ β (π β π)βπ€ β (π β π) Β¬ π€(πβπ)π§)) |
38 | | ssdif0 4328 |
. . . . . . . . . . . . . . 15
β’ ((π β© (β‘(πβπ) β {π§})) β π β ((π β© (β‘(πβπ) β {π§})) β π) = β
) |
39 | | indif1 4236 |
. . . . . . . . . . . . . . . 16
β’ ((π β π) β© (β‘(πβπ) β {π§})) = ((π β© (β‘(πβπ) β {π§})) β π) |
40 | 39 | eqeq1i 2742 |
. . . . . . . . . . . . . . 15
β’ (((π β π) β© (β‘(πβπ) β {π§})) = β
β ((π β© (β‘(πβπ) β {π§})) β π) = β
) |
41 | | disj 4412 |
. . . . . . . . . . . . . . . 16
β’ (((π β π) β© (β‘(πβπ) β {π§})) = β
β βπ€ β (π β π) Β¬ π€ β (β‘(πβπ) β {π§})) |
42 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . 20
β’ π€ β V |
43 | 42 | eliniseg 6051 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β V β (π€ β (β‘(πβπ) β {π§}) β π€(πβπ)π§)) |
44 | 43 | elv 3454 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β (β‘(πβπ) β {π§}) β π€(πβπ)π§) |
45 | 44 | notbii 320 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π€ β (β‘(πβπ) β {π§}) β Β¬ π€(πβπ)π§) |
46 | 45 | ralbii 3097 |
. . . . . . . . . . . . . . . 16
β’
(βπ€ β
(π β π) Β¬ π€ β (β‘(πβπ) β {π§}) β βπ€ β (π β π) Β¬ π€(πβπ)π§) |
47 | 41, 46 | bitri 275 |
. . . . . . . . . . . . . . 15
β’ (((π β π) β© (β‘(πβπ) β {π§})) = β
β βπ€ β (π β π) Β¬ π€(πβπ)π§) |
48 | 38, 40, 47 | 3bitr2i 299 |
. . . . . . . . . . . . . 14
β’ ((π β© (β‘(πβπ) β {π§})) β π β βπ€ β (π β π) Β¬ π€(πβπ)π§) |
49 | | cnvimass 6038 |
. . . . . . . . . . . . . . . . 17
β’ (β‘(πβπ) β {π§}) β dom (πβπ) |
50 | 26 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (πβπ) β (π Γ π)) |
51 | | dmss 5863 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ) β (π Γ π) β dom (πβπ) β dom (π Γ π)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β dom (πβπ) β dom (π Γ π)) |
53 | | dmxpid 5890 |
. . . . . . . . . . . . . . . . . 18
β’ dom
(π Γ π) = π |
54 | 52, 53 | sseqtrdi 3999 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β dom (πβπ) β π) |
55 | 49, 54 | sstrid 3960 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (β‘(πβπ) β {π§}) β π) |
56 | | sseqin2 4180 |
. . . . . . . . . . . . . . . 16
β’ ((β‘(πβπ) β {π§}) β π β (π β© (β‘(πβπ) β {π§})) = (β‘(πβπ) β {π§})) |
57 | 55, 56 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (π β© (β‘(πβπ) β {π§})) = (β‘(πβπ) β {π§})) |
58 | 57 | sseq1d 3980 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β ((π β© (β‘(πβπ) β {π§})) β π β (β‘(πβπ) β {π§}) β π)) |
59 | 48, 58 | bitr3id 285 |
. . . . . . . . . . . . 13
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (βπ€ β (π β π) Β¬ π€(πβπ)π§ β (β‘(πβπ) β {π§}) β π)) |
60 | 59 | rexbidv 3176 |
. . . . . . . . . . . 12
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (βπ§ β (π β π)βπ€ β (π β π) Β¬ π€(πβπ)π§ β βπ§ β (π β π)(β‘(πβπ) β {π§}) β π)) |
61 | | eldifn 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ β (π β π) β Β¬ π§ β π) |
62 | 61 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β Β¬ π§ β π) |
63 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ = π§ β (π€ β π β π§ β π)) |
64 | 63 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ = π§ β (Β¬ π€ β π β Β¬ π§ β π)) |
65 | 62, 64 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (π€ = π§ β Β¬ π€ β π)) |
66 | 65 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (π€ β π β Β¬ π€ = π§)) |
67 | 66 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β Β¬ π€ = π§) |
68 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β Β¬ π§ β π) |
69 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β π
= ((πβπ) β© (π Γ π))) |
70 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π
= ((πβπ) β© (π Γ π))) |
71 | 70 | breqd 5121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (π§π
π€ β π§((πβπ) β© (π Γ π))π€)) |
72 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ β (π β π) β π§ β π) |
73 | 72 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π§ β π) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π§ β π) |
75 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π€ β π) |
76 | | brxp 5686 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§(π Γ π)π€ β (π§ β π β§ π€ β π)) |
77 | 74, 75, 76 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π§(π Γ π)π€) |
78 | | brin 5162 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§((πβπ) β© (π Γ π))π€ β (π§(πβπ)π€ β§ π§(π Γ π)π€)) |
79 | 78 | rbaib 540 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§(π Γ π)π€ β (π§((πβπ) β© (π Γ π))π€ β π§(πβπ)π€)) |
80 | 77, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (π§((πβπ) β© (π Γ π))π€ β π§(πβπ)π€)) |
81 | 71, 80 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (π§π
π€ β π§(πβπ)π€)) |
82 | 1, 2 | fpwwe2lem2 10575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (πππ
β ((π β π΄ β§ π
β (π Γ π)) β§ (π
We π β§ βπ¦ β π [(β‘π
β {π¦}) / π’](π’πΉ(π
β© (π’ Γ π’))) = π¦)))) |
83 | 82 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ πππ
) β ((π β π΄ β§ π
β (π Γ π)) β§ (π
We π β§ βπ¦ β π [(β‘π
β {π¦}) / π’](π’πΉ(π
β© (π’ Γ π’))) = π¦))) |
84 | 83 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β ((π β π΄ β§ π
β (π Γ π)) β§ (π
We π β§ βπ¦ β π [(β‘π
β {π¦}) / π’](π’πΉ(π
β© (π’ Γ π’))) = π¦))) |
85 | 84 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β (π β π΄ β§ π
β (π Γ π))) |
86 | 85 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β π
β (π Γ π)) |
87 | 86 | ad5ant12 755 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π
β (π Γ π)) |
88 | 87 | ssbrd 5153 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (π§π
π€ β π§(π Γ π)π€)) |
89 | | brxp 5686 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§(π Γ π)π€ β (π§ β π β§ π€ β π)) |
90 | 89 | simplbi 499 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§(π Γ π)π€ β π§ β π) |
91 | 88, 90 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (π§π
π€ β π§ β π)) |
92 | 81, 91 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (π§(πβπ)π€ β π§ β π)) |
93 | 68, 92 | mtod 197 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β Β¬ π§(πβπ)π€) |
94 | 31 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (πβπ) We π) |
95 | | weso 5629 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πβπ) We π β (πβπ) Or π) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (πβπ) Or π) |
97 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π β π) |
98 | 97 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π€ β π) |
99 | | sotric 5578 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ) Or π β§ (π€ β π β§ π§ β π)) β (π€(πβπ)π§ β Β¬ (π€ = π§ β¨ π§(πβπ)π€))) |
100 | | ioran 983 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
(π€ = π§ β¨ π§(πβπ)π€) β (Β¬ π€ = π§ β§ Β¬ π§(πβπ)π€)) |
101 | 99, 100 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πβπ) Or π β§ (π€ β π β§ π§ β π)) β (π€(πβπ)π§ β (Β¬ π€ = π§ β§ Β¬ π§(πβπ)π€))) |
102 | 96, 98, 74, 101 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β (π€(πβπ)π§ β (Β¬ π€ = π§ β§ Β¬ π§(πβπ)π€))) |
103 | 67, 93, 102 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π€(πβπ)π§) |
104 | 103, 44 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π€ β π) β π€ β (β‘(πβπ) β {π§})) |
105 | 104 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (π€ β π β π€ β (β‘(πβπ) β {π§}))) |
106 | 105 | ssrdv 3955 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π β (β‘(πβπ) β {π§})) |
107 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (β‘(πβπ) β {π§}) β π) |
108 | 106, 107 | eqssd 3966 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π = (β‘(πβπ) β {π§})) |
109 | | in32 4186 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ) β© (π Γ π)) β© (π Γ π)) = (((πβπ) β© (π Γ π)) β© (π Γ π)) |
110 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π
= ((πβπ) β© (π Γ π))) |
111 | 110 | ineq1d 4176 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (π
β© (π Γ π)) = (((πβπ) β© (π Γ π)) β© (π Γ π))) |
112 | 86 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π
β (π Γ π)) |
113 | | df-ss 3932 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β (π Γ π) β (π
β© (π Γ π)) = π
) |
114 | 112, 113 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (π
β© (π Γ π)) = π
) |
115 | 111, 114 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (((πβπ) β© (π Γ π)) β© (π Γ π)) = π
) |
116 | | inss2 4194 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβπ) β© (π Γ π)) β (π Γ π) |
117 | | xpss1 5657 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β (π Γ π) β (π Γ π)) |
118 | 97, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (π Γ π) β (π Γ π)) |
119 | 116, 118 | sstrid 3960 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β ((πβπ) β© (π Γ π)) β (π Γ π)) |
120 | | df-ss 3932 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβπ) β© (π Γ π)) β (π Γ π) β (((πβπ) β© (π Γ π)) β© (π Γ π)) = ((πβπ) β© (π Γ π))) |
121 | 119, 120 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (((πβπ) β© (π Γ π)) β© (π Γ π)) = ((πβπ) β© (π Γ π))) |
122 | 109, 115,
121 | 3eqtr3a 2801 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π
= ((πβπ) β© (π Γ π))) |
123 | 108 | sqxpeqd 5670 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (π Γ π) = ((β‘(πβπ) β {π§}) Γ (β‘(πβπ) β {π§}))) |
124 | 123 | ineq2d 4177 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β ((πβπ) β© (π Γ π)) = ((πβπ) β© ((β‘(πβπ) β {π§}) Γ (β‘(πβπ) β {π§})))) |
125 | 122, 124 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π
= ((πβπ) β© ((β‘(πβπ) β {π§}) Γ (β‘(πβπ) β {π§})))) |
126 | 108, 125 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (ππΉπ
) = ((β‘(πβπ) β {π§})πΉ((πβπ) β© ((β‘(πβπ) β {π§}) Γ (β‘(πβπ) β {π§}))))) |
127 | 18 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β π΄ β π) |
128 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β ππ(πβπ)) |
129 | 128 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β ππ(πβπ)) |
130 | 1, 127, 129 | fpwwe2lem3 10576 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β§ π§ β π) β ((β‘(πβπ) β {π§})πΉ((πβπ) β© ((β‘(πβπ) β {π§}) Γ (β‘(πβπ) β {π§})))) = π§) |
131 | 73, 130 | mpdan 686 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β ((β‘(πβπ) β {π§})πΉ((πβπ) β© ((β‘(πβπ) β {π§}) Γ (β‘(πβπ) β {π§})))) = π§) |
132 | 126, 131 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β (ππΉπ
) = π§) |
133 | 132, 62 | eqneltrd 2858 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β§ (π§ β (π β π) β§ (β‘(πβπ) β {π§}) β π)) β Β¬ (ππΉπ
) β π) |
134 | 133 | rexlimdvaa 3154 |
. . . . . . . . . . . 12
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (βπ§ β (π β π)(β‘(πβπ) β {π§}) β π β Β¬ (ππΉπ
) β π)) |
135 | 60, 134 | sylbid 239 |
. . . . . . . . . . 11
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (βπ§ β (π β π)βπ€ β (π β π) Β¬ π€(πβπ)π§ β Β¬ (ππΉπ
) β π)) |
136 | 37, 135 | syld 47 |
. . . . . . . . . 10
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β ((π β π) β β
β Β¬ (ππΉπ
) β π)) |
137 | 136 | necon4ad 2963 |
. . . . . . . . 9
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β ((ππΉπ
) β π β (π β π) = β
)) |
138 | 16, 137 | mpd 15 |
. . . . . . . 8
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β (π β π) = β
) |
139 | | ssdif0 4328 |
. . . . . . . 8
β’ (π β π β (π β π) = β
) |
140 | 138, 139 | sylibr 233 |
. . . . . . 7
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π β π β§ π
= ((πβπ) β© (π Γ π)))) β π β π) |
141 | 140 | ex 414 |
. . . . . 6
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β ((π β π β§ π
= ((πβπ) β© (π Γ π))) β π β π)) |
142 | 3 | adantlr 714 |
. . . . . . 7
β’ (((π β§ (πππ
β§ (ππΉπ
) β π)) β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) |
143 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β πππ
) |
144 | 1, 17, 142, 128, 143 | fpwwe2lem9 10582 |
. . . . . 6
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β ((π β π β§ (πβπ) = (π
β© (π Γ π))) β¨ (π β π β§ π
= ((πβπ) β© (π Γ π))))) |
145 | 15, 141, 144 | mpjaod 859 |
. . . . 5
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β π β π) |
146 | 13, 145 | eqssd 3966 |
. . . 4
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β π = π) |
147 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β Fun π) |
148 | 146, 143 | eqbrtrrd 5134 |
. . . . . 6
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β πππ
) |
149 | | funbrfv 6898 |
. . . . . 6
β’ (Fun
π β (πππ
β (πβπ) = π
)) |
150 | 147, 148,
149 | sylc 65 |
. . . . 5
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β (πβπ) = π
) |
151 | 150 | eqcomd 2743 |
. . . 4
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β π
= (πβπ)) |
152 | 146, 151 | jca 513 |
. . 3
β’ ((π β§ (πππ
β§ (ππΉπ
) β π)) β (π = π β§ π
= (πβπ))) |
153 | 152 | ex 414 |
. 2
β’ (π β ((πππ
β§ (ππΉπ
) β π) β (π = π β§ π
= (πβπ)))) |
154 | 1, 2, 3, 4 | fpwwe2lem12 10585 |
. . . 4
β’ (π β (ππΉ(πβπ)) β π) |
155 | 22, 154 | jca 513 |
. . 3
β’ (π β (ππ(πβπ) β§ (ππΉ(πβπ)) β π)) |
156 | | breq12 5115 |
. . . 4
β’ ((π = π β§ π
= (πβπ)) β (πππ
β ππ(πβπ))) |
157 | | oveq12 7371 |
. . . . 5
β’ ((π = π β§ π
= (πβπ)) β (ππΉπ
) = (ππΉ(πβπ))) |
158 | | simpl 484 |
. . . . 5
β’ ((π = π β§ π
= (πβπ)) β π = π) |
159 | 157, 158 | eleq12d 2832 |
. . . 4
β’ ((π = π β§ π
= (πβπ)) β ((ππΉπ
) β π β (ππΉ(πβπ)) β π)) |
160 | 156, 159 | anbi12d 632 |
. . 3
β’ ((π = π β§ π
= (πβπ)) β ((πππ
β§ (ππΉπ
) β π) β (ππ(πβπ) β§ (ππΉ(πβπ)) β π))) |
161 | 155, 160 | syl5ibrcom 247 |
. 2
β’ (π β ((π = π β§ π
= (πβπ)) β (πππ
β§ (ππΉπ
) β π))) |
162 | 153, 161 | impbid 211 |
1
β’ (π β ((πππ
β§ (ππΉπ
) β π) β (π = π β§ π
= (πβπ)))) |