Step | Hyp | Ref
| Expression |
1 | | issmfge.s |
. . . . . . 7
β’ (π β π β SAlg) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (SMblFnβπ)) β π β SAlg) |
3 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ β (SMblFnβπ)) |
4 | | issmfge.d |
. . . . . 6
β’ π· = dom πΉ |
5 | 2, 3, 4 | smfdmss 45048 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β π· β βͺ π) |
6 | 2, 3, 4 | smff 45047 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ:π·βΆβ) |
7 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦π |
8 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦ πΉ β (SMblFnβπ) |
9 | 7, 8 | nfan 1903 |
. . . . . . . 8
β’
β²π¦(π β§ πΉ β (SMblFnβπ)) |
10 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦ π β β |
11 | 9, 10 | nfan 1903 |
. . . . . . 7
β’
β²π¦((π β§ πΉ β (SMblFnβπ)) β§ π β β) |
12 | | nfv 1918 |
. . . . . . 7
β’
β²π((π β§ πΉ β (SMblFnβπ)) β§ π β β) |
13 | 1 | uniexd 7684 |
. . . . . . . . . . . 12
β’ (π β βͺ π
β V) |
14 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π· β βͺ π) β βͺ π
β V) |
15 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π· β βͺ π) β π· β βͺ π) |
16 | 14, 15 | ssexd 5286 |
. . . . . . . . . 10
β’ ((π β§ π· β βͺ π) β π· β V) |
17 | 5, 16 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ πΉ β (SMblFnβπ)) β π· β V) |
18 | | eqid 2737 |
. . . . . . . . 9
β’ (π βΎt π·) = (π βΎt π·) |
19 | 2, 17, 18 | subsalsal 44674 |
. . . . . . . 8
β’ ((π β§ πΉ β (SMblFnβπ)) β (π βΎt π·) β SAlg) |
20 | 19 | adantr 482 |
. . . . . . 7
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β (π βΎt π·) β SAlg) |
21 | 6 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π¦ β π·) β (πΉβπ¦) β β) |
22 | 21 | rexrd 11212 |
. . . . . . . 8
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π¦ β π·) β (πΉβπ¦) β
β*) |
23 | 22 | adantlr 714 |
. . . . . . 7
β’ ((((π β§ πΉ β (SMblFnβπ)) β§ π β β) β§ π¦ β π·) β (πΉβπ¦) β
β*) |
24 | 2 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β π β SAlg) |
25 | 3 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β πΉ β (SMblFnβπ)) |
26 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β π β β) |
27 | 24, 25, 4, 26 | smfpreimagt 45077 |
. . . . . . . 8
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β {π¦ β π· β£ π < (πΉβπ¦)} β (π βΎt π·)) |
28 | 27 | adantlr 714 |
. . . . . . 7
β’ ((((π β§ πΉ β (SMblFnβπ)) β§ π β β) β§ π β β) β {π¦ β π· β£ π < (πΉβπ¦)} β (π βΎt π·)) |
29 | | simpr 486 |
. . . . . . 7
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β π β β) |
30 | 11, 12, 20, 23, 28, 29 | salpreimagtge 45040 |
. . . . . 6
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) |
31 | 30 | ralrimiva 3144 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) |
32 | 5, 6, 31 | 3jca 1129 |
. . . 4
β’ ((π β§ πΉ β (SMblFnβπ)) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) |
33 | 32 | ex 414 |
. . 3
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)))) |
34 | | nfv 1918 |
. . . . . . 7
β’
β²π¦ π· β βͺ π |
35 | | nfv 1918 |
. . . . . . 7
β’
β²π¦ πΉ:π·βΆβ |
36 | | nfcv 2908 |
. . . . . . . 8
β’
β²π¦β |
37 | | nfrab1 3429 |
. . . . . . . . 9
β’
β²π¦{π¦ β π· β£ π β€ (πΉβπ¦)} |
38 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π¦(π βΎt π·) |
39 | 37, 38 | nfel 2922 |
. . . . . . . 8
β’
β²π¦{π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·) |
40 | 36, 39 | nfralw 3297 |
. . . . . . 7
β’
β²π¦βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·) |
41 | 34, 35, 40 | nf3an 1905 |
. . . . . 6
β’
β²π¦(π· β βͺ π
β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) |
42 | 7, 41 | nfan 1903 |
. . . . 5
β’
β²π¦(π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) |
43 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
44 | | nfv 1918 |
. . . . . . 7
β’
β²π π· β βͺ π |
45 | | nfv 1918 |
. . . . . . 7
β’
β²π πΉ:π·βΆβ |
46 | | nfra1 3270 |
. . . . . . 7
β’
β²πβπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·) |
47 | 44, 45, 46 | nf3an 1905 |
. . . . . 6
β’
β²π(π· β βͺ π
β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) |
48 | 43, 47 | nfan 1903 |
. . . . 5
β’
β²π(π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) |
49 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) β π β SAlg) |
50 | | simpr1 1195 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) β π· β βͺ π) |
51 | | simpr2 1196 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) β πΉ:π·βΆβ) |
52 | | simpr3 1197 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) β βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) |
53 | 42, 48, 49, 4, 50, 51, 52 | issmfgelem 45084 |
. . . 4
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·))) β πΉ β (SMblFnβπ)) |
54 | 53 | ex 414 |
. . 3
β’ (π β ((π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) β πΉ β (SMblFnβπ))) |
55 | 33, 54 | impbid 211 |
. 2
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)))) |
56 | | breq1 5113 |
. . . . . . . 8
β’ (π = π β (π β€ (πΉβπ¦) β π β€ (πΉβπ¦))) |
57 | 56 | rabbidv 3418 |
. . . . . . 7
β’ (π = π β {π¦ β π· β£ π β€ (πΉβπ¦)} = {π¦ β π· β£ π β€ (πΉβπ¦)}) |
58 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
59 | 58 | breq2d 5122 |
. . . . . . . . 9
β’ (π¦ = π₯ β (π β€ (πΉβπ¦) β π β€ (πΉβπ₯))) |
60 | 59 | cbvrabv 3420 |
. . . . . . . 8
β’ {π¦ β π· β£ π β€ (πΉβπ¦)} = {π₯ β π· β£ π β€ (πΉβπ₯)} |
61 | 60 | a1i 11 |
. . . . . . 7
β’ (π = π β {π¦ β π· β£ π β€ (πΉβπ¦)} = {π₯ β π· β£ π β€ (πΉβπ₯)}) |
62 | 57, 61 | eqtrd 2777 |
. . . . . 6
β’ (π = π β {π¦ β π· β£ π β€ (πΉβπ¦)} = {π₯ β π· β£ π β€ (πΉβπ₯)}) |
63 | 62 | eleq1d 2823 |
. . . . 5
β’ (π = π β ({π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·) β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·))) |
64 | 63 | cbvralvw 3228 |
. . . 4
β’
(βπ β
β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·) β βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·)) |
65 | 64 | 3anbi3i 1160 |
. . 3
β’ ((π· β βͺ π
β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·))) |
66 | 65 | a1i 11 |
. 2
β’ (π β ((π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ π β€ (πΉβπ¦)} β (π βΎt π·)) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·)))) |
67 | 55, 66 | bitrd 279 |
1
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·)))) |