Step | Hyp | Ref
| Expression |
1 | | 3anrot 1101 |
. . . . . . . . . . . . 13
β’ ((π¦ β π β§ π β π β§ π β π) β (π β π β§ π β π β§ π¦ β π)) |
2 | | ordtval.1 |
. . . . . . . . . . . . . 14
β’ π = dom π
|
3 | 2 | tsrlemax 18482 |
. . . . . . . . . . . . 13
β’ ((π
β TosetRel β§ (π¦ β π β§ π β π β§ π β π)) β (π¦π
if(ππ
π, π, π) β (π¦π
π β¨ π¦π
π))) |
4 | 1, 3 | sylan2br 596 |
. . . . . . . . . . . 12
β’ ((π
β TosetRel β§ (π β π β§ π β π β§ π¦ β π)) β (π¦π
if(ππ
π, π, π) β (π¦π
π β¨ π¦π
π))) |
5 | 4 | 3exp2 1355 |
. . . . . . . . . . 11
β’ (π
β TosetRel β (π β π β (π β π β (π¦ β π β (π¦π
if(ππ
π, π, π) β (π¦π
π β¨ π¦π
π)))))) |
6 | 5 | imp42 428 |
. . . . . . . . . 10
β’ (((π
β TosetRel β§ (π β π β§ π β π)) β§ π¦ β π) β (π¦π
if(ππ
π, π, π) β (π¦π
π β¨ π¦π
π))) |
7 | 6 | notbid 318 |
. . . . . . . . 9
β’ (((π
β TosetRel β§ (π β π β§ π β π)) β§ π¦ β π) β (Β¬ π¦π
if(ππ
π, π, π) β Β¬ (π¦π
π β¨ π¦π
π))) |
8 | | ioran 983 |
. . . . . . . . 9
β’ (Β¬
(π¦π
π β¨ π¦π
π) β (Β¬ π¦π
π β§ Β¬ π¦π
π)) |
9 | 7, 8 | bitrdi 287 |
. . . . . . . 8
β’ (((π
β TosetRel β§ (π β π β§ π β π)) β§ π¦ β π) β (Β¬ π¦π
if(ππ
π, π, π) β (Β¬ π¦π
π β§ Β¬ π¦π
π))) |
10 | 9 | rabbidva 3417 |
. . . . . . 7
β’ ((π
β TosetRel β§ (π β π β§ π β π)) β {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)} = {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)}) |
11 | | ifcl 4536 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β if(ππ
π, π, π) β π) |
12 | 11 | ancoms 460 |
. . . . . . . 8
β’ ((π β π β§ π β π) β if(ππ
π, π, π) β π) |
13 | | dmexg 7845 |
. . . . . . . . . . . 12
β’ (π
β TosetRel β dom
π
β
V) |
14 | 2, 13 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ (π
β TosetRel β π β V) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π
β TosetRel β§ (π β π β§ π β π)) β π β V) |
16 | | rabexg 5293 |
. . . . . . . . . 10
β’ (π β V β {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β V) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
β’ ((π
β TosetRel β§ (π β π β§ π β π)) β {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β V) |
18 | 10, 17 | eqeltrd 2838 |
. . . . . . . 8
β’ ((π
β TosetRel β§ (π β π β§ π β π)) β {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)} β V) |
19 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) = (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) |
20 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π₯ = if(ππ
π, π, π) β (π¦π
π₯ β π¦π
if(ππ
π, π, π))) |
21 | 20 | notbid 318 |
. . . . . . . . . . 11
β’ (π₯ = if(ππ
π, π, π) β (Β¬ π¦π
π₯ β Β¬ π¦π
if(ππ
π, π, π))) |
22 | 21 | rabbidv 3418 |
. . . . . . . . . 10
β’ (π₯ = if(ππ
π, π, π) β {π¦ β π β£ Β¬ π¦π
π₯} = {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)}) |
23 | 19, 22 | elrnmpt1s 5917 |
. . . . . . . . 9
β’
((if(ππ
π, π, π) β π β§ {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)} β V) β {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)} β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})) |
24 | | ordtval.2 |
. . . . . . . . 9
β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) |
25 | 23, 24 | eleqtrrdi 2849 |
. . . . . . . 8
β’
((if(ππ
π, π, π) β π β§ {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)} β V) β {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)} β π΄) |
26 | 12, 18, 25 | syl2an2 685 |
. . . . . . 7
β’ ((π
β TosetRel β§ (π β π β§ π β π)) β {π¦ β π β£ Β¬ π¦π
if(ππ
π, π, π)} β π΄) |
27 | 10, 26 | eqeltrrd 2839 |
. . . . . 6
β’ ((π
β TosetRel β§ (π β π β§ π β π)) β {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β π΄) |
28 | 27 | ralrimivva 3198 |
. . . . 5
β’ (π
β TosetRel β
βπ β π βπ β π {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β π΄) |
29 | | rabexg 5293 |
. . . . . . . 8
β’ (π β V β {π¦ β π β£ Β¬ π¦π
π} β V) |
30 | 14, 29 | syl 17 |
. . . . . . 7
β’ (π
β TosetRel β {π¦ β π β£ Β¬ π¦π
π} β V) |
31 | 30 | ralrimivw 3148 |
. . . . . 6
β’ (π
β TosetRel β
βπ β π {π¦ β π β£ Β¬ π¦π
π} β V) |
32 | | breq2 5114 |
. . . . . . . . . 10
β’ (π₯ = π β (π¦π
π₯ β π¦π
π)) |
33 | 32 | notbid 318 |
. . . . . . . . 9
β’ (π₯ = π β (Β¬ π¦π
π₯ β Β¬ π¦π
π)) |
34 | 33 | rabbidv 3418 |
. . . . . . . 8
β’ (π₯ = π β {π¦ β π β£ Β¬ π¦π
π₯} = {π¦ β π β£ Β¬ π¦π
π}) |
35 | 34 | cbvmptv 5223 |
. . . . . . 7
β’ (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) = (π β π β¦ {π¦ β π β£ Β¬ π¦π
π}) |
36 | | ineq1 4170 |
. . . . . . . . . 10
β’ (π§ = {π¦ β π β£ Β¬ π¦π
π} β (π§ β© {π¦ β π β£ Β¬ π¦π
π}) = ({π¦ β π β£ Β¬ π¦π
π} β© {π¦ β π β£ Β¬ π¦π
π})) |
37 | | inrab 4271 |
. . . . . . . . . 10
β’ ({π¦ β π β£ Β¬ π¦π
π} β© {π¦ β π β£ Β¬ π¦π
π}) = {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} |
38 | 36, 37 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π§ = {π¦ β π β£ Β¬ π¦π
π} β (π§ β© {π¦ β π β£ Β¬ π¦π
π}) = {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)}) |
39 | 38 | eleq1d 2823 |
. . . . . . . 8
β’ (π§ = {π¦ β π β£ Β¬ π¦π
π} β ((π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄ β {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β π΄)) |
40 | 39 | ralbidv 3175 |
. . . . . . 7
β’ (π§ = {π¦ β π β£ Β¬ π¦π
π} β (βπ β π (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄ β βπ β π {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β π΄)) |
41 | 35, 40 | ralrnmptw 7049 |
. . . . . 6
β’
(βπ β
π {π¦ β π β£ Β¬ π¦π
π} β V β (βπ§ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})βπ β π (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄ β βπ β π βπ β π {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β π΄)) |
42 | 31, 41 | syl 17 |
. . . . 5
β’ (π
β TosetRel β
(βπ§ β ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})βπ β π (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄ β βπ β π βπ β π {π¦ β π β£ (Β¬ π¦π
π β§ Β¬ π¦π
π)} β π΄)) |
43 | 28, 42 | mpbird 257 |
. . . 4
β’ (π
β TosetRel β
βπ§ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})βπ β π (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄) |
44 | | rabexg 5293 |
. . . . . . . 8
β’ (π β V β {π¦ β π β£ Β¬ π¦π
π} β V) |
45 | 14, 44 | syl 17 |
. . . . . . 7
β’ (π
β TosetRel β {π¦ β π β£ Β¬ π¦π
π} β V) |
46 | 45 | ralrimivw 3148 |
. . . . . 6
β’ (π
β TosetRel β
βπ β π {π¦ β π β£ Β¬ π¦π
π} β V) |
47 | | breq2 5114 |
. . . . . . . . . 10
β’ (π₯ = π β (π¦π
π₯ β π¦π
π)) |
48 | 47 | notbid 318 |
. . . . . . . . 9
β’ (π₯ = π β (Β¬ π¦π
π₯ β Β¬ π¦π
π)) |
49 | 48 | rabbidv 3418 |
. . . . . . . 8
β’ (π₯ = π β {π¦ β π β£ Β¬ π¦π
π₯} = {π¦ β π β£ Β¬ π¦π
π}) |
50 | 49 | cbvmptv 5223 |
. . . . . . 7
β’ (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) = (π β π β¦ {π¦ β π β£ Β¬ π¦π
π}) |
51 | | ineq2 4171 |
. . . . . . . 8
β’ (π€ = {π¦ β π β£ Β¬ π¦π
π} β (π§ β© π€) = (π§ β© {π¦ β π β£ Β¬ π¦π
π})) |
52 | 51 | eleq1d 2823 |
. . . . . . 7
β’ (π€ = {π¦ β π β£ Β¬ π¦π
π} β ((π§ β© π€) β π΄ β (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄)) |
53 | 50, 52 | ralrnmptw 7049 |
. . . . . 6
β’
(βπ β
π {π¦ β π β£ Β¬ π¦π
π} β V β (βπ€ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})(π§ β© π€) β π΄ β βπ β π (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄)) |
54 | 46, 53 | syl 17 |
. . . . 5
β’ (π
β TosetRel β
(βπ€ β ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})(π§ β© π€) β π΄ β βπ β π (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄)) |
55 | 54 | ralbidv 3175 |
. . . 4
β’ (π
β TosetRel β
(βπ§ β ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})βπ€ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})(π§ β© π€) β π΄ β βπ§ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})βπ β π (π§ β© {π¦ β π β£ Β¬ π¦π
π}) β π΄)) |
56 | 43, 55 | mpbird 257 |
. . 3
β’ (π
β TosetRel β
βπ§ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})βπ€ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})(π§ β© π€) β π΄) |
57 | 24 | raleqi 3314 |
. . . 4
β’
(βπ€ β
π΄ (π§ β© π€) β π΄ β βπ€ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})(π§ β© π€) β π΄) |
58 | 24, 57 | raleqbii 3318 |
. . 3
β’
(βπ§ β
π΄ βπ€ β π΄ (π§ β© π€) β π΄ β βπ§ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})βπ€ β ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯})(π§ β© π€) β π΄) |
59 | 56, 58 | sylibr 233 |
. 2
β’ (π
β TosetRel β
βπ§ β π΄ βπ€ β π΄ (π§ β© π€) β π΄) |
60 | 14 | pwexd 5339 |
. . . 4
β’ (π
β TosetRel β
π« π β
V) |
61 | | ssrab2 4042 |
. . . . . . . 8
β’ {π¦ β π β£ Β¬ π¦π
π₯} β π |
62 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π
β TosetRel β§ π₯ β π) β π β V) |
63 | | elpw2g 5306 |
. . . . . . . . 9
β’ (π β V β ({π¦ β π β£ Β¬ π¦π
π₯} β π« π β {π¦ β π β£ Β¬ π¦π
π₯} β π)) |
64 | 62, 63 | syl 17 |
. . . . . . . 8
β’ ((π
β TosetRel β§ π₯ β π) β ({π¦ β π β£ Β¬ π¦π
π₯} β π« π β {π¦ β π β£ Β¬ π¦π
π₯} β π)) |
65 | 61, 64 | mpbiri 258 |
. . . . . . 7
β’ ((π
β TosetRel β§ π₯ β π) β {π¦ β π β£ Β¬ π¦π
π₯} β π« π) |
66 | 65 | fmpttd 7068 |
. . . . . 6
β’ (π
β TosetRel β (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}):πβΆπ« π) |
67 | 66 | frnd 6681 |
. . . . 5
β’ (π
β TosetRel β ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) β π« π) |
68 | 24, 67 | eqsstrid 3997 |
. . . 4
β’ (π
β TosetRel β π΄ β π« π) |
69 | 60, 68 | ssexd 5286 |
. . 3
β’ (π
β TosetRel β π΄ β V) |
70 | | inficl 9368 |
. . 3
β’ (π΄ β V β (βπ§ β π΄ βπ€ β π΄ (π§ β© π€) β π΄ β (fiβπ΄) = π΄)) |
71 | 69, 70 | syl 17 |
. 2
β’ (π
β TosetRel β
(βπ§ β π΄ βπ€ β π΄ (π§ β© π€) β π΄ β (fiβπ΄) = π΄)) |
72 | 59, 71 | mpbid 231 |
1
β’ (π
β TosetRel β
(fiβπ΄) = π΄) |