Step | Hyp | Ref
| Expression |
1 | | dfiin2g 5035 |
. . 3
β’
(βπ¦ β
πΌ π β πΆ β β©
π¦ β πΌ π = β© {π β£ βπ¦ β πΌ π = π}) |
2 | 1 | 3ad2ant3 1135 |
. 2
β’ ((πΆ β (Mooreβπ) β§ πΌ β β
β§ βπ¦ β πΌ π β πΆ) β β©
π¦ β πΌ π = β© {π β£ βπ¦ β πΌ π = π}) |
3 | | simp1 1136 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ πΌ β β
β§ βπ¦ β πΌ π β πΆ) β πΆ β (Mooreβπ)) |
4 | | uniiunlem 4084 |
. . . . 5
β’
(βπ¦ β
πΌ π β πΆ β (βπ¦ β πΌ π β πΆ β {π β£ βπ¦ β πΌ π = π} β πΆ)) |
5 | 4 | ibi 266 |
. . . 4
β’
(βπ¦ β
πΌ π β πΆ β {π β£ βπ¦ β πΌ π = π} β πΆ) |
6 | 5 | 3ad2ant3 1135 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ πΌ β β
β§ βπ¦ β πΌ π β πΆ) β {π β£ βπ¦ β πΌ π = π} β πΆ) |
7 | | n0 4346 |
. . . . . 6
β’ (πΌ β β
β
βπ¦ π¦ β πΌ) |
8 | | nfra1 3281 |
. . . . . . . 8
β’
β²π¦βπ¦ β πΌ π β πΆ |
9 | | nfre1 3282 |
. . . . . . . . . 10
β’
β²π¦βπ¦ β πΌ π = π |
10 | 9 | nfab 2909 |
. . . . . . . . 9
β’
β²π¦{π β£ βπ¦ β πΌ π = π} |
11 | | nfcv 2903 |
. . . . . . . . 9
β’
β²π¦β
|
12 | 10, 11 | nfne 3043 |
. . . . . . . 8
β’
β²π¦{π β£ βπ¦ β πΌ π = π} β β
|
13 | 8, 12 | nfim 1899 |
. . . . . . 7
β’
β²π¦(βπ¦ β πΌ π β πΆ β {π β£ βπ¦ β πΌ π = π} β β
) |
14 | | rsp 3244 |
. . . . . . . . . 10
β’
(βπ¦ β
πΌ π β πΆ β (π¦ β πΌ β π β πΆ)) |
15 | 14 | com12 32 |
. . . . . . . . 9
β’ (π¦ β πΌ β (βπ¦ β πΌ π β πΆ β π β πΆ)) |
16 | | elisset 2815 |
. . . . . . . . . . 11
β’ (π β πΆ β βπ π = π) |
17 | | rspe 3246 |
. . . . . . . . . . . 12
β’ ((π¦ β πΌ β§ βπ π = π) β βπ¦ β πΌ βπ π = π) |
18 | 17 | ex 413 |
. . . . . . . . . . 11
β’ (π¦ β πΌ β (βπ π = π β βπ¦ β πΌ βπ π = π)) |
19 | 16, 18 | syl5 34 |
. . . . . . . . . 10
β’ (π¦ β πΌ β (π β πΆ β βπ¦ β πΌ βπ π = π)) |
20 | | rexcom4 3285 |
. . . . . . . . . 10
β’
(βπ¦ β
πΌ βπ π = π β βπ βπ¦ β πΌ π = π) |
21 | 19, 20 | imbitrdi 250 |
. . . . . . . . 9
β’ (π¦ β πΌ β (π β πΆ β βπ βπ¦ β πΌ π = π)) |
22 | 15, 21 | syld 47 |
. . . . . . . 8
β’ (π¦ β πΌ β (βπ¦ β πΌ π β πΆ β βπ βπ¦ β πΌ π = π)) |
23 | | abn0 4380 |
. . . . . . . 8
β’ ({π β£ βπ¦ β πΌ π = π} β β
β βπ βπ¦ β πΌ π = π) |
24 | 22, 23 | imbitrrdi 251 |
. . . . . . 7
β’ (π¦ β πΌ β (βπ¦ β πΌ π β πΆ β {π β£ βπ¦ β πΌ π = π} β β
)) |
25 | 13, 24 | exlimi 2210 |
. . . . . 6
β’
(βπ¦ π¦ β πΌ β (βπ¦ β πΌ π β πΆ β {π β£ βπ¦ β πΌ π = π} β β
)) |
26 | 7, 25 | sylbi 216 |
. . . . 5
β’ (πΌ β β
β
(βπ¦ β πΌ π β πΆ β {π β£ βπ¦ β πΌ π = π} β β
)) |
27 | 26 | imp 407 |
. . . 4
β’ ((πΌ β β
β§
βπ¦ β πΌ π β πΆ) β {π β£ βπ¦ β πΌ π = π} β β
) |
28 | 27 | 3adant1 1130 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ πΌ β β
β§ βπ¦ β πΌ π β πΆ) β {π β£ βπ¦ β πΌ π = π} β β
) |
29 | | mreintcl 17541 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ {π β£ βπ¦ β πΌ π = π} β πΆ β§ {π β£ βπ¦ β πΌ π = π} β β
) β β© {π
β£ βπ¦ β
πΌ π = π} β πΆ) |
30 | 3, 6, 28, 29 | syl3anc 1371 |
. 2
β’ ((πΆ β (Mooreβπ) β§ πΌ β β
β§ βπ¦ β πΌ π β πΆ) β β© {π β£ βπ¦ β πΌ π = π} β πΆ) |
31 | 2, 30 | eqeltrd 2833 |
1
β’ ((πΆ β (Mooreβπ) β§ πΌ β β
β§ βπ¦ β πΌ π β πΆ) β β©
π¦ β πΌ π β πΆ) |