Step | Hyp | Ref
| Expression |
1 | | ssrab2 4078 |
. . . 4
β’ {π β π« π β£ βͺ (πΉ
β (π« π β©
Fin)) β π } β
π« π |
2 | 1 | a1i 11 |
. . 3
β’ ((π β π β§ πΉ:π« πβΆπ« π) β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β π« π) |
3 | | pweq 4617 |
. . . . . . . 8
β’ (π = (π β© β© π‘) β π« π = π« (π β© β© π‘)) |
4 | 3 | ineq1d 4212 |
. . . . . . 7
β’ (π = (π β© β© π‘) β (π« π β© Fin) = (π« (π β© β© π‘)
β© Fin)) |
5 | 4 | imaeq2d 6060 |
. . . . . 6
β’ (π = (π β© β© π‘) β (πΉ β (π« π β© Fin)) = (πΉ β (π« (π β© β© π‘) β© Fin))) |
6 | 5 | unieqd 4923 |
. . . . 5
β’ (π = (π β© β© π‘) β βͺ (πΉ
β (π« π β©
Fin)) = βͺ (πΉ β (π« (π β© β© π‘) β© Fin))) |
7 | | id 22 |
. . . . 5
β’ (π = (π β© β© π‘) β π = (π β© β© π‘)) |
8 | 6, 7 | sseq12d 4016 |
. . . 4
β’ (π = (π β© β© π‘) β (βͺ (πΉ
β (π« π β©
Fin)) β π β
βͺ (πΉ β (π« (π β© β© π‘) β© Fin)) β (π β© β© π‘))) |
9 | | inss1 4229 |
. . . . . 6
β’ (π β© β© π‘)
β π |
10 | | elpw2g 5345 |
. . . . . 6
β’ (π β π β ((π β© β© π‘) β π« π β (π β© β© π‘) β π)) |
11 | 9, 10 | mpbiri 258 |
. . . . 5
β’ (π β π β (π β© β© π‘) β π« π) |
12 | 11 | ad2antrr 725 |
. . . 4
β’ (((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β (π β© β© π‘) β π« π) |
13 | | imassrn 6071 |
. . . . . . . . 9
β’ (πΉ β (π« (π β© β© π‘)
β© Fin)) β ran πΉ |
14 | | frn 6725 |
. . . . . . . . . 10
β’ (πΉ:π« πβΆπ« π β ran πΉ β π« π) |
15 | 14 | adantl 483 |
. . . . . . . . 9
β’ ((π β π β§ πΉ:π« πβΆπ« π) β ran πΉ β π« π) |
16 | 13, 15 | sstrid 3994 |
. . . . . . . 8
β’ ((π β π β§ πΉ:π« πβΆπ« π) β (πΉ β (π« (π β© β© π‘) β© Fin)) β π«
π) |
17 | 16 | unissd 4919 |
. . . . . . 7
β’ ((π β π β§ πΉ:π« πβΆπ« π) β βͺ (πΉ β (π« (π β© β© π‘)
β© Fin)) β βͺ π« π) |
18 | | unipw 5451 |
. . . . . . 7
β’ βͺ π« π = π |
19 | 17, 18 | sseqtrdi 4033 |
. . . . . 6
β’ ((π β π β§ πΉ:π« πβΆπ« π) β βͺ (πΉ β (π« (π β© β© π‘)
β© Fin)) β π) |
20 | 19 | adantr 482 |
. . . . 5
β’ (((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β βͺ (πΉ
β (π« (π β©
β© π‘) β© Fin)) β π) |
21 | | inss2 4230 |
. . . . . . . . . . . . . 14
β’ (π β© β© π‘)
β β© π‘ |
22 | | intss1 4968 |
. . . . . . . . . . . . . 14
β’ (π β π‘ β β© π‘ β π) |
23 | 21, 22 | sstrid 3994 |
. . . . . . . . . . . . 13
β’ (π β π‘ β (π β© β© π‘) β π) |
24 | 23 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β§ π β π‘) β (π β© β© π‘) β π) |
25 | 24 | sspwd 4616 |
. . . . . . . . . . 11
β’ ((((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β§ π β π‘) β π« (π β© β© π‘) β π« π) |
26 | 25 | ssrind 4236 |
. . . . . . . . . 10
β’ ((((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β§ π β π‘) β (π« (π β© β© π‘) β© Fin) β (π«
π β©
Fin)) |
27 | | imass2 6102 |
. . . . . . . . . 10
β’
((π« (π β©
β© π‘) β© Fin) β (π« π β© Fin) β (πΉ β (π« (π β© β© π‘)
β© Fin)) β (πΉ
β (π« π β©
Fin))) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
β’ ((((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β§ π β π‘) β (πΉ β (π« (π β© β© π‘) β© Fin)) β (πΉ β (π« π β© Fin))) |
29 | 28 | unissd 4919 |
. . . . . . . 8
β’ ((((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β§ π β π‘) β βͺ (πΉ β (π« (π β© β© π‘)
β© Fin)) β βͺ (πΉ β (π« π β© Fin))) |
30 | | ssel2 3978 |
. . . . . . . . . 10
β’ ((π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β§ π β π‘) β π β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) |
31 | | pweq 4617 |
. . . . . . . . . . . . . . . 16
β’ (π = π β π« π = π« π) |
32 | 31 | ineq1d 4212 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π« π β© Fin) = (π« π β© Fin)) |
33 | 32 | imaeq2d 6060 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉ β (π« π β© Fin)) = (πΉ β (π« π β© Fin))) |
34 | 33 | unieqd 4923 |
. . . . . . . . . . . . 13
β’ (π = π β βͺ (πΉ β (π« π β© Fin)) = βͺ (πΉ
β (π« π β©
Fin))) |
35 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = π β π = π) |
36 | 34, 35 | sseq12d 4016 |
. . . . . . . . . . . 12
β’ (π = π β (βͺ (πΉ β (π« π β© Fin)) β π β βͺ (πΉ
β (π« π β©
Fin)) β π)) |
37 | 36 | elrab 3684 |
. . . . . . . . . . 11
β’ (π β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β (π β π« π β§ βͺ (πΉ β (π« π β© Fin)) β π)) |
38 | 37 | simprbi 498 |
. . . . . . . . . 10
β’ (π β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (πΉ
β (π« π β©
Fin)) β π) |
39 | 30, 38 | syl 17 |
. . . . . . . . 9
β’ ((π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β§ π β π‘) β βͺ (πΉ β (π« π β© Fin)) β π) |
40 | 39 | adantll 713 |
. . . . . . . 8
β’ ((((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β§ π β π‘) β βͺ (πΉ β (π« π β© Fin)) β π) |
41 | 29, 40 | sstrd 3993 |
. . . . . . 7
β’ ((((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β§ π β π‘) β βͺ (πΉ β (π« (π β© β© π‘)
β© Fin)) β π) |
42 | 41 | ralrimiva 3147 |
. . . . . 6
β’ (((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β βπ β π‘ βͺ (πΉ β (π« (π β© β© π‘)
β© Fin)) β π) |
43 | | ssint 4969 |
. . . . . 6
β’ (βͺ (πΉ
β (π« (π β©
β© π‘) β© Fin)) β β© π‘
β βπ β
π‘ βͺ (πΉ
β (π« (π β©
β© π‘) β© Fin)) β π) |
44 | 42, 43 | sylibr 233 |
. . . . 5
β’ (((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β βͺ (πΉ
β (π« (π β©
β© π‘) β© Fin)) β β© π‘) |
45 | 20, 44 | ssind 4233 |
. . . 4
β’ (((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β βͺ (πΉ
β (π« (π β©
β© π‘) β© Fin)) β (π β© β© π‘)) |
46 | 8, 12, 45 | elrabd 3686 |
. . 3
β’ (((π β π β§ πΉ:π« πβΆπ« π) β§ π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) β (π β© β© π‘) β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π }) |
47 | 2, 46 | ismred2 17547 |
. 2
β’ ((π β π β§ πΉ:π« πβΆπ« π) β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β (Mooreβπ)) |
48 | | fssxp 6746 |
. . . 4
β’ (πΉ:π« πβΆπ« π β πΉ β (π« π Γ π« π)) |
49 | | pwexg 5377 |
. . . . 5
β’ (π β π β π« π β V) |
50 | 49, 49 | xpexd 7738 |
. . . 4
β’ (π β π β (π« π Γ π« π) β V) |
51 | | ssexg 5324 |
. . . 4
β’ ((πΉ β (π« π Γ π« π) β§ (π« π Γ π« π) β V) β πΉ β V) |
52 | 48, 50, 51 | syl2anr 598 |
. . 3
β’ ((π β π β§ πΉ:π« πβΆπ« π) β πΉ β V) |
53 | | simpr 486 |
. . . 4
β’ ((π β π β§ πΉ:π« πβΆπ« π) β πΉ:π« πβΆπ« π) |
54 | | pweq 4617 |
. . . . . . . . . 10
β’ (π = π‘ β π« π = π« π‘) |
55 | 54 | ineq1d 4212 |
. . . . . . . . 9
β’ (π = π‘ β (π« π β© Fin) = (π« π‘ β© Fin)) |
56 | 55 | imaeq2d 6060 |
. . . . . . . 8
β’ (π = π‘ β (πΉ β (π« π β© Fin)) = (πΉ β (π« π‘ β© Fin))) |
57 | 56 | unieqd 4923 |
. . . . . . 7
β’ (π = π‘ β βͺ (πΉ β (π« π β© Fin)) = βͺ (πΉ
β (π« π‘ β©
Fin))) |
58 | | id 22 |
. . . . . . 7
β’ (π = π‘ β π = π‘) |
59 | 57, 58 | sseq12d 4016 |
. . . . . 6
β’ (π = π‘ β (βͺ (πΉ β (π« π β© Fin)) β π β βͺ (πΉ
β (π« π‘ β©
Fin)) β π‘)) |
60 | 59 | elrab3 3685 |
. . . . 5
β’ (π‘ β π« π β (π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (πΉ
β (π« π‘ β©
Fin)) β π‘)) |
61 | 60 | rgen 3064 |
. . . 4
β’
βπ‘ β
π« π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (πΉ
β (π« π‘ β©
Fin)) β π‘) |
62 | 53, 61 | jctir 522 |
. . 3
β’ ((π β π β§ πΉ:π« πβΆπ« π) β (πΉ:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (πΉ
β (π« π‘ β©
Fin)) β π‘))) |
63 | | feq1 6699 |
. . . 4
β’ (π = πΉ β (π:π« πβΆπ« π β πΉ:π« πβΆπ« π)) |
64 | | imaeq1 6055 |
. . . . . . . 8
β’ (π = πΉ β (π β (π« π‘ β© Fin)) = (πΉ β (π« π‘ β© Fin))) |
65 | 64 | unieqd 4923 |
. . . . . . 7
β’ (π = πΉ β βͺ (π β (π« π‘ β© Fin)) = βͺ (πΉ
β (π« π‘ β©
Fin))) |
66 | 65 | sseq1d 4014 |
. . . . . 6
β’ (π = πΉ β (βͺ (π β (π« π‘ β© Fin)) β π‘ β βͺ (πΉ
β (π« π‘ β©
Fin)) β π‘)) |
67 | 66 | bibi2d 343 |
. . . . 5
β’ (π = πΉ β ((π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (π
β (π« π‘ β©
Fin)) β π‘) β
(π‘ β {π β π« π β£ βͺ (πΉ
β (π« π β©
Fin)) β π } β
βͺ (πΉ β (π« π‘ β© Fin)) β π‘))) |
68 | 67 | ralbidv 3178 |
. . . 4
β’ (π = πΉ β (βπ‘ β π« π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (π
β (π« π‘ β©
Fin)) β π‘) β
βπ‘ β π«
π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (πΉ
β (π« π‘ β©
Fin)) β π‘))) |
69 | 63, 68 | anbi12d 632 |
. . 3
β’ (π = πΉ β ((π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (π
β (π« π‘ β©
Fin)) β π‘)) β
(πΉ:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (πΉ
β (π« π‘ β©
Fin)) β π‘)))) |
70 | 52, 62, 69 | spcedv 3589 |
. 2
β’ ((π β π β§ πΉ:π« πβΆπ« π) β βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (π
β (π« π‘ β©
Fin)) β π‘))) |
71 | | isacs 17595 |
. 2
β’ ({π β π« π β£ βͺ (πΉ
β (π« π β©
Fin)) β π } β
(ACSβπ) β
({π β π« π β£ βͺ (πΉ
β (π« π β©
Fin)) β π } β
(Mooreβπ) β§
βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β βͺ (π
β (π« π‘ β©
Fin)) β π‘)))) |
72 | 47, 70, 71 | sylanbrc 584 |
1
β’ ((π β π β§ πΉ:π« πβΆπ« π) β {π β π« π β£ βͺ (πΉ β (π« π β© Fin)) β π } β (ACSβπ)) |