Step | Hyp | Ref
| Expression |
1 | | fveq2 6890 |
. . 3
β’ (π₯ = π β (ACSβπ₯) = (ACSβπ)) |
2 | | pweq 4615 |
. . . 4
β’ (π₯ = π β π« π₯ = π« π) |
3 | 2 | fveq2d 6894 |
. . 3
β’ (π₯ = π β (Mooreβπ« π₯) = (Mooreβπ« π)) |
4 | 1, 3 | eleq12d 2825 |
. 2
β’ (π₯ = π β ((ACSβπ₯) β (Mooreβπ« π₯) β (ACSβπ) β (Mooreβπ«
π))) |
5 | | acsmre 17600 |
. . . . . . 7
β’ (π β (ACSβπ₯) β π β (Mooreβπ₯)) |
6 | | mresspw 17540 |
. . . . . . . 8
β’ (π β (Mooreβπ₯) β π β π« π₯) |
7 | 5, 6 | syl 17 |
. . . . . . 7
β’ (π β (ACSβπ₯) β π β π« π₯) |
8 | 5, 7 | elpwd 4607 |
. . . . . 6
β’ (π β (ACSβπ₯) β π β π« π« π₯) |
9 | 8 | ssriv 3985 |
. . . . 5
β’
(ACSβπ₯)
β π« π« π₯ |
10 | 9 | a1i 11 |
. . . 4
β’ (β€
β (ACSβπ₯)
β π« π« π₯) |
11 | | vex 3476 |
. . . . . . . 8
β’ π₯ β V |
12 | | mremre 17552 |
. . . . . . . 8
β’ (π₯ β V β
(Mooreβπ₯) β
(Mooreβπ« π₯)) |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
β’ (π β (ACSβπ₯) β (Mooreβπ₯) β (Mooreβπ«
π₯)) |
14 | 5 | ssriv 3985 |
. . . . . . . 8
β’
(ACSβπ₯)
β (Mooreβπ₯) |
15 | | sstr 3989 |
. . . . . . . 8
β’ ((π β (ACSβπ₯) β§ (ACSβπ₯) β (Mooreβπ₯)) β π β (Mooreβπ₯)) |
16 | 14, 15 | mpan2 687 |
. . . . . . 7
β’ (π β (ACSβπ₯) β π β (Mooreβπ₯)) |
17 | | mrerintcl 17545 |
. . . . . . 7
β’
(((Mooreβπ₯)
β (Mooreβπ« π₯) β§ π β (Mooreβπ₯)) β (π« π₯ β© β© π) β (Mooreβπ₯)) |
18 | 13, 16, 17 | syl2anc 582 |
. . . . . 6
β’ (π β (ACSβπ₯) β (π« π₯ β© β© π)
β (Mooreβπ₯)) |
19 | | ssel2 3976 |
. . . . . . . . . . . . . . . 16
β’ ((π β (ACSβπ₯) β§ π β π) β π β (ACSβπ₯)) |
20 | 19 | acsmred 17604 |
. . . . . . . . . . . . . . 15
β’ ((π β (ACSβπ₯) β§ π β π) β π β (Mooreβπ₯)) |
21 | | eqid 2730 |
. . . . . . . . . . . . . . 15
β’
(mrClsβπ) =
(mrClsβπ) |
22 | 20, 21 | mrcssvd 17571 |
. . . . . . . . . . . . . 14
β’ ((π β (ACSβπ₯) β§ π β π) β ((mrClsβπ)βπ) β π₯) |
23 | 22 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ (π β (ACSβπ₯) β βπ β π ((mrClsβπ)βπ) β π₯) |
24 | 23 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β βπ β π ((mrClsβπ)βπ) β π₯) |
25 | | iunss 5047 |
. . . . . . . . . . . 12
β’ (βͺ π β π ((mrClsβπ)βπ) β π₯ β βπ β π ((mrClsβπ)βπ) β π₯) |
26 | 24, 25 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β βͺ
π β π ((mrClsβπ)βπ) β π₯) |
27 | 11 | elpw2 5344 |
. . . . . . . . . . 11
β’ (βͺ π β π ((mrClsβπ)βπ) β π« π₯ β βͺ
π β π ((mrClsβπ)βπ) β π₯) |
28 | 26, 27 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β βͺ
π β π ((mrClsβπ)βπ) β π« π₯) |
29 | 28 | fmpttd 7115 |
. . . . . . . . 9
β’ (π β (ACSβπ₯) β (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)):π« π₯βΆπ« π₯) |
30 | | fssxp 6744 |
. . . . . . . . 9
β’ ((π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)):π« π₯βΆπ« π₯ β (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (π« π₯ Γ π« π₯)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’ (π β (ACSβπ₯) β (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (π« π₯ Γ π« π₯)) |
32 | | vpwex 5374 |
. . . . . . . . 9
β’ π«
π₯ β V |
33 | 32, 32 | xpex 7742 |
. . . . . . . 8
β’
(π« π₯ Γ
π« π₯) β
V |
34 | | ssexg 5322 |
. . . . . . . 8
β’ (((π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) β (π« π₯ Γ π« π₯) β§ (π« π₯ Γ π« π₯) β V) β (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β V) |
35 | 31, 33, 34 | sylancl 584 |
. . . . . . 7
β’ (π β (ACSβπ₯) β (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β V) |
36 | 19 | adantlr 711 |
. . . . . . . . . . . . 13
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β π) β π β (ACSβπ₯)) |
37 | | elpwi 4608 |
. . . . . . . . . . . . . 14
β’ (π β π« π₯ β π β π₯) |
38 | 37 | ad2antlr 723 |
. . . . . . . . . . . . 13
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β π) β π β π₯) |
39 | 21 | acsfiel2 17603 |
. . . . . . . . . . . . 13
β’ ((π β (ACSβπ₯) β§ π β π₯) β (π β π β βπ β (π« π β© Fin)((mrClsβπ)βπ) β π)) |
40 | 36, 38, 39 | syl2anc 582 |
. . . . . . . . . . . 12
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β π) β (π β π β βπ β (π« π β© Fin)((mrClsβπ)βπ) β π)) |
41 | 40 | ralbidva 3173 |
. . . . . . . . . . 11
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (βπ β π π β π β βπ β π βπ β (π« π β© Fin)((mrClsβπ)βπ) β π)) |
42 | | iunss 5047 |
. . . . . . . . . . . . 13
β’ (βͺ π β π ((mrClsβπ)βπ) β π β βπ β π ((mrClsβπ)βπ) β π) |
43 | 42 | ralbii 3091 |
. . . . . . . . . . . 12
β’
(βπ β
(π« π β©
Fin)βͺ π β π ((mrClsβπ)βπ) β π β βπ β (π« π β© Fin)βπ β π ((mrClsβπ)βπ) β π) |
44 | | ralcom 3284 |
. . . . . . . . . . . 12
β’
(βπ β
(π« π β©
Fin)βπ β π ((mrClsβπ)βπ) β π β βπ β π βπ β (π« π β© Fin)((mrClsβπ)βπ) β π) |
45 | 43, 44 | bitri 274 |
. . . . . . . . . . 11
β’
(βπ β
(π« π β©
Fin)βͺ π β π ((mrClsβπ)βπ) β π β βπ β π βπ β (π« π β© Fin)((mrClsβπ)βπ) β π) |
46 | 41, 45 | bitr4di 288 |
. . . . . . . . . 10
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (βπ β π π β π β βπ β (π« π β© Fin)βͺ π β π ((mrClsβπ)βπ) β π)) |
47 | | elrint2 4995 |
. . . . . . . . . . 11
β’ (π β π« π₯ β (π β (π« π₯ β© β© π) β βπ β π π β π)) |
48 | 47 | adantl 480 |
. . . . . . . . . 10
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (π β (π« π₯ β© β© π) β βπ β π π β π)) |
49 | | funmpt 6585 |
. . . . . . . . . . . . 13
β’ Fun
(π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) |
50 | | funiunfv 7249 |
. . . . . . . . . . . . 13
β’ (Fun
(π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) β βͺ
π β (π« π β© Fin)((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) = βͺ ((π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin))) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . 12
β’ βͺ π β (π« π β© Fin)((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) = βͺ ((π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) |
52 | 51 | sseq1i 4009 |
. . . . . . . . . . 11
β’ (βͺ π β (π« π β© Fin)((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) β π β βͺ ((π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π) |
53 | | iunss 5047 |
. . . . . . . . . . . 12
β’ (βͺ π β (π« π β© Fin)((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) β π β βπ β (π« π β© Fin)((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) β π) |
54 | | eqid 2730 |
. . . . . . . . . . . . . . 15
β’ (π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) |
55 | | fveq2 6890 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((mrClsβπ)βπ) = ((mrClsβπ)βπ)) |
56 | 55 | iuneq2d 5025 |
. . . . . . . . . . . . . . 15
β’ (π = π β βͺ
π β π ((mrClsβπ)βπ) = βͺ π β π ((mrClsβπ)βπ)) |
57 | | inss1 4227 |
. . . . . . . . . . . . . . . . 17
β’
(π« π β©
Fin) β π« π |
58 | 37 | sspwd 4614 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π« π₯ β π« π β π« π₯) |
59 | 58 | adantl 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β π« π β π« π₯) |
60 | 57, 59 | sstrid 3992 |
. . . . . . . . . . . . . . . 16
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (π« π β© Fin) β π« π₯) |
61 | 60 | sselda 3981 |
. . . . . . . . . . . . . . 15
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β (π« π β© Fin)) β π β π« π₯) |
62 | 20, 21 | mrcssvd 17571 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (ACSβπ₯) β§ π β π) β ((mrClsβπ)βπ) β π₯) |
63 | 62 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (ACSβπ₯) β βπ β π ((mrClsβπ)βπ) β π₯) |
64 | 63 | ad2antrr 722 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β (π« π β© Fin)) β βπ β π ((mrClsβπ)βπ) β π₯) |
65 | | iunss 5047 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ π β π ((mrClsβπ)βπ) β π₯ β βπ β π ((mrClsβπ)βπ) β π₯) |
66 | 64, 65 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β (π« π β© Fin)) β βͺ π β π ((mrClsβπ)βπ) β π₯) |
67 | | ssexg 5322 |
. . . . . . . . . . . . . . . 16
β’
((βͺ π β π ((mrClsβπ)βπ) β π₯ β§ π₯ β V) β βͺ π β π ((mrClsβπ)βπ) β V) |
68 | 66, 11, 67 | sylancl 584 |
. . . . . . . . . . . . . . 15
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β (π« π β© Fin)) β βͺ π β π ((mrClsβπ)βπ) β V) |
69 | 54, 56, 61, 68 | fvmptd3 7020 |
. . . . . . . . . . . . . 14
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β (π« π β© Fin)) β ((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) = βͺ π β π ((mrClsβπ)βπ)) |
70 | 69 | sseq1d 4012 |
. . . . . . . . . . . . 13
β’ (((π β (ACSβπ₯) β§ π β π« π₯) β§ π β (π« π β© Fin)) β (((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) β π β βͺ
π β π ((mrClsβπ)βπ) β π)) |
71 | 70 | ralbidva 3173 |
. . . . . . . . . . . 12
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (βπ β (π« π β© Fin)((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) β π β βπ β (π« π β© Fin)βͺ π β π ((mrClsβπ)βπ) β π)) |
72 | 53, 71 | bitrid 282 |
. . . . . . . . . . 11
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (βͺ
π β (π« π β© Fin)((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ))βπ) β π β βπ β (π« π β© Fin)βͺ π β π ((mrClsβπ)βπ) β π)) |
73 | 52, 72 | bitr3id 284 |
. . . . . . . . . 10
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (βͺ
((π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π β βπ β (π« π β© Fin)βͺ π β π ((mrClsβπ)βπ) β π)) |
74 | 46, 48, 73 | 3bitr4d 310 |
. . . . . . . . 9
β’ ((π β (ACSβπ₯) β§ π β π« π₯) β (π β (π« π₯ β© β© π) β βͺ ((π
β π« π₯ β¦
βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π)) |
75 | 74 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β (ACSβπ₯) β βπ β π« π₯(π β (π« π₯ β© β© π) β βͺ ((π
β π« π₯ β¦
βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π)) |
76 | 29, 75 | jca 510 |
. . . . . . 7
β’ (π β (ACSβπ₯) β ((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)):π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β (π« π₯ β© β© π) β βͺ ((π
β π« π₯ β¦
βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π))) |
77 | | feq1 6697 |
. . . . . . . 8
β’ (π = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (π:π« π₯βΆπ« π₯ β (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)):π« π₯βΆπ« π₯)) |
78 | | imaeq1 6053 |
. . . . . . . . . . . 12
β’ (π = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (π β (π« π β© Fin)) = ((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (π« π β© Fin))) |
79 | 78 | unieqd 4921 |
. . . . . . . . . . 11
β’ (π = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β βͺ (π β (π« π β© Fin)) = βͺ ((π
β π« π₯ β¦
βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin))) |
80 | 79 | sseq1d 4012 |
. . . . . . . . . 10
β’ (π = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (βͺ
(π β (π« π β© Fin)) β π β βͺ ((π
β π« π₯ β¦
βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π)) |
81 | 80 | bibi2d 341 |
. . . . . . . . 9
β’ (π = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β ((π β (π« π₯ β© β© π) β βͺ (π
β (π« π β©
Fin)) β π) β
(π β (π« π₯ β© β© π)
β βͺ ((π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π))) |
82 | 81 | ralbidv 3175 |
. . . . . . . 8
β’ (π = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β (βπ β π« π₯(π β (π« π₯ β© β© π) β βͺ (π
β (π« π β©
Fin)) β π) β
βπ β π«
π₯(π β (π« π₯ β© β© π) β βͺ ((π
β π« π₯ β¦
βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π))) |
83 | 77, 82 | anbi12d 629 |
. . . . . . 7
β’ (π = (π β π« π₯ β¦ βͺ
π β π ((mrClsβπ)βπ)) β ((π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β (π« π₯ β© β© π) β βͺ (π
β (π« π β©
Fin)) β π)) β
((π β π« π₯ β¦ βͺ π β π ((mrClsβπ)βπ)):π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β (π« π₯ β© β© π) β βͺ ((π
β π« π₯ β¦
βͺ π β π ((mrClsβπ)βπ)) β (π« π β© Fin)) β π)))) |
84 | 35, 76, 83 | spcedv 3587 |
. . . . . 6
β’ (π β (ACSβπ₯) β βπ(π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β (π« π₯ β© β© π) β βͺ (π
β (π« π β©
Fin)) β π))) |
85 | | isacs 17599 |
. . . . . 6
β’
((π« π₯ β©
β© π) β (ACSβπ₯) β ((π« π₯ β© β© π) β (Mooreβπ₯) β§ βπ(π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β (π« π₯ β© β© π) β βͺ (π
β (π« π β©
Fin)) β π)))) |
86 | 18, 84, 85 | sylanbrc 581 |
. . . . 5
β’ (π β (ACSβπ₯) β (π« π₯ β© β© π)
β (ACSβπ₯)) |
87 | 86 | adantl 480 |
. . . 4
β’
((β€ β§ π
β (ACSβπ₯))
β (π« π₯ β©
β© π) β (ACSβπ₯)) |
88 | 10, 87 | ismred2 17551 |
. . 3
β’ (β€
β (ACSβπ₯) β
(Mooreβπ« π₯)) |
89 | 88 | mptru 1546 |
. 2
β’
(ACSβπ₯) β
(Mooreβπ« π₯) |
90 | 4, 89 | vtoclg 3541 |
1
β’ (π β π β (ACSβπ) β (Mooreβπ« π)) |