Step | Hyp | Ref
| Expression |
1 | | mclsppslem.10 |
. . . 4
β’ (π β π β ran πΏ) |
2 | | mclspps.l |
. . . . 5
β’ πΏ = (mSubstβπ) |
3 | | mclspps.e |
. . . . 5
β’ πΈ = (mExβπ) |
4 | 2, 3 | msubf 34166 |
. . . 4
β’ (π β ran πΏ β π :πΈβΆπΈ) |
5 | 1, 4 | syl 17 |
. . 3
β’ (π β π :πΈβΆπΈ) |
6 | | mclspps.1 |
. . . . . . . 8
β’ (π β π β mFS) |
7 | | eqid 2737 |
. . . . . . . . 9
β’
(mAxβπ) =
(mAxβπ) |
8 | | eqid 2737 |
. . . . . . . . 9
β’
(mStatβπ) =
(mStatβπ) |
9 | 7, 8 | maxsta 34188 |
. . . . . . . 8
β’ (π β mFS β
(mAxβπ) β
(mStatβπ)) |
10 | 6, 9 | syl 17 |
. . . . . . 7
β’ (π β (mAxβπ) β (mStatβπ)) |
11 | | eqid 2737 |
. . . . . . . 8
β’
(mPreStβπ) =
(mPreStβπ) |
12 | 11, 8 | mstapst 34181 |
. . . . . . 7
β’
(mStatβπ)
β (mPreStβπ) |
13 | 10, 12 | sstrdi 3961 |
. . . . . 6
β’ (π β (mAxβπ) β (mPreStβπ)) |
14 | | mclsppslem.9 |
. . . . . 6
β’ (π β β¨π, π, πβ© β (mAxβπ)) |
15 | 13, 14 | sseldd 3950 |
. . . . 5
β’ (π β β¨π, π, πβ© β (mPreStβπ)) |
16 | | mclspps.d |
. . . . . 6
β’ π· = (mDVβπ) |
17 | 16, 3, 11 | elmpst 34170 |
. . . . 5
β’
(β¨π, π, πβ© β (mPreStβπ) β ((π β π· β§ β‘π = π) β§ (π β πΈ β§ π β Fin) β§ π β πΈ)) |
18 | 15, 17 | sylib 217 |
. . . 4
β’ (π β ((π β π· β§ β‘π = π) β§ (π β πΈ β§ π β Fin) β§ π β πΈ)) |
19 | 18 | simp3d 1145 |
. . 3
β’ (π β π β πΈ) |
20 | 5, 19 | ffvelcdmd 7041 |
. 2
β’ (π β (π βπ) β πΈ) |
21 | | fvco3 6945 |
. . . 4
β’ ((π :πΈβΆπΈ β§ π β πΈ) β ((π β π )βπ) = (πβ(π βπ))) |
22 | 5, 19, 21 | syl2anc 585 |
. . 3
β’ (π β ((π β π )βπ) = (πβ(π βπ))) |
23 | | mclspps.c |
. . . 4
β’ πΆ = (mClsβπ) |
24 | | mclspps.2 |
. . . 4
β’ (π β πΎ β π·) |
25 | | mclspps.3 |
. . . 4
β’ (π β π΅ β πΈ) |
26 | | mclspps.v |
. . . 4
β’ π = (mVRβπ) |
27 | | mclspps.h |
. . . 4
β’ π» = (mVHβπ) |
28 | | mclspps.w |
. . . 4
β’ π = (mVarsβπ) |
29 | | mclspps.5 |
. . . . 5
β’ (π β π β ran πΏ) |
30 | 2 | msubco 34165 |
. . . . 5
β’ ((π β ran πΏ β§ π β ran πΏ) β (π β π ) β ran πΏ) |
31 | 29, 1, 30 | syl2anc 585 |
. . . 4
β’ (π β (π β π ) β ran πΏ) |
32 | 2, 3 | msubf 34166 |
. . . . . . . . 9
β’ (π β ran πΏ β π:πΈβΆπΈ) |
33 | 29, 32 | syl 17 |
. . . . . . . 8
β’ (π β π:πΈβΆπΈ) |
34 | | fco 6697 |
. . . . . . . 8
β’ ((π:πΈβΆπΈ β§ π :πΈβΆπΈ) β (π β π ):πΈβΆπΈ) |
35 | 33, 5, 34 | syl2anc 585 |
. . . . . . 7
β’ (π β (π β π ):πΈβΆπΈ) |
36 | 35 | ffnd 6674 |
. . . . . 6
β’ (π β (π β π ) Fn πΈ) |
37 | 36 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β (π β π ) Fn πΈ) |
38 | | mclsppslem.11 |
. . . . . . . . 9
β’ (π β (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) |
39 | 5 | ffund 6677 |
. . . . . . . . . 10
β’ (π β Fun π ) |
40 | 17 | simp2bi 1147 |
. . . . . . . . . . . . . 14
β’
(β¨π, π, πβ© β (mPreStβπ) β (π β πΈ β§ π β Fin)) |
41 | 15, 40 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π β πΈ β§ π β Fin)) |
42 | 41 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β π β πΈ) |
43 | 26, 3, 27 | mvhf 34192 |
. . . . . . . . . . . . 13
β’ (π β mFS β π»:πβΆπΈ) |
44 | | frn 6680 |
. . . . . . . . . . . . 13
β’ (π»:πβΆπΈ β ran π» β πΈ) |
45 | 6, 43, 44 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β ran π» β πΈ) |
46 | 42, 45 | unssd 4151 |
. . . . . . . . . . 11
β’ (π β (π βͺ ran π») β πΈ) |
47 | 5 | fdmd 6684 |
. . . . . . . . . . 11
β’ (π β dom π = πΈ) |
48 | 46, 47 | sseqtrrd 3990 |
. . . . . . . . . 10
β’ (π β (π βͺ ran π») β dom π ) |
49 | | funimass3 7009 |
. . . . . . . . . 10
β’ ((Fun
π β§ (π βͺ ran π») β dom π ) β ((π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅)) β (π βͺ ran π») β (β‘π β (β‘π β (πΎπΆπ΅))))) |
50 | 39, 48, 49 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅)) β (π βͺ ran π») β (β‘π β (β‘π β (πΎπΆπ΅))))) |
51 | 38, 50 | mpbid 231 |
. . . . . . . 8
β’ (π β (π βͺ ran π») β (β‘π β (β‘π β (πΎπΆπ΅)))) |
52 | | cnvco 5846 |
. . . . . . . . . 10
β’ β‘(π β π ) = (β‘π β β‘π) |
53 | 52 | imaeq1i 6015 |
. . . . . . . . 9
β’ (β‘(π β π ) β (πΎπΆπ΅)) = ((β‘π β β‘π) β (πΎπΆπ΅)) |
54 | | imaco 6208 |
. . . . . . . . 9
β’ ((β‘π β β‘π) β (πΎπΆπ΅)) = (β‘π β (β‘π β (πΎπΆπ΅))) |
55 | 53, 54 | eqtri 2765 |
. . . . . . . 8
β’ (β‘(π β π ) β (πΎπΆπ΅)) = (β‘π β (β‘π β (πΎπΆπ΅))) |
56 | 51, 55 | sseqtrrdi 4000 |
. . . . . . 7
β’ (π β (π βͺ ran π») β (β‘(π β π ) β (πΎπΆπ΅))) |
57 | 56 | unssad 4152 |
. . . . . 6
β’ (π β π β (β‘(π β π ) β (πΎπΆπ΅))) |
58 | 57 | sselda 3949 |
. . . . 5
β’ ((π β§ π β π) β π β (β‘(π β π ) β (πΎπΆπ΅))) |
59 | | elpreima 7013 |
. . . . . 6
β’ ((π β π ) Fn πΈ β (π β (β‘(π β π ) β (πΎπΆπ΅)) β (π β πΈ β§ ((π β π )βπ) β (πΎπΆπ΅)))) |
60 | 59 | simplbda 501 |
. . . . 5
β’ (((π β π ) Fn πΈ β§ π β (β‘(π β π ) β (πΎπΆπ΅))) β ((π β π )βπ) β (πΎπΆπ΅)) |
61 | 37, 58, 60 | syl2anc 585 |
. . . 4
β’ ((π β§ π β π) β ((π β π )βπ) β (πΎπΆπ΅)) |
62 | 36 | adantr 482 |
. . . . 5
β’ ((π β§ π‘ β π) β (π β π ) Fn πΈ) |
63 | 56 | unssbd 4153 |
. . . . . . 7
β’ (π β ran π» β (β‘(π β π ) β (πΎπΆπ΅))) |
64 | 63 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β ran π» β (β‘(π β π ) β (πΎπΆπ΅))) |
65 | | ffn 6673 |
. . . . . . . 8
β’ (π»:πβΆπΈ β π» Fn π) |
66 | 6, 43, 65 | 3syl 18 |
. . . . . . 7
β’ (π β π» Fn π) |
67 | | fnfvelrn 7036 |
. . . . . . 7
β’ ((π» Fn π β§ π‘ β π) β (π»βπ‘) β ran π») |
68 | 66, 67 | sylan 581 |
. . . . . 6
β’ ((π β§ π‘ β π) β (π»βπ‘) β ran π») |
69 | 64, 68 | sseldd 3950 |
. . . . 5
β’ ((π β§ π‘ β π) β (π»βπ‘) β (β‘(π β π ) β (πΎπΆπ΅))) |
70 | | elpreima 7013 |
. . . . . 6
β’ ((π β π ) Fn πΈ β ((π»βπ‘) β (β‘(π β π ) β (πΎπΆπ΅)) β ((π»βπ‘) β πΈ β§ ((π β π )β(π»βπ‘)) β (πΎπΆπ΅)))) |
71 | 70 | simplbda 501 |
. . . . 5
β’ (((π β π ) Fn πΈ β§ (π»βπ‘) β (β‘(π β π ) β (πΎπΆπ΅))) β ((π β π )β(π»βπ‘)) β (πΎπΆπ΅)) |
72 | 62, 69, 71 | syl2anc 585 |
. . . 4
β’ ((π β§ π‘ β π) β ((π β π )β(π»βπ‘)) β (πΎπΆπ΅)) |
73 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ πππ) β π :πΈβΆπΈ) |
74 | 6, 43 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π»:πβΆπΈ) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ πππ) β π»:πβΆπΈ) |
76 | 18 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β π· β§ β‘π = π)) |
77 | 76 | simpld 496 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π·) |
78 | 26, 16 | mdvval 34138 |
. . . . . . . . . . . . . . . . . . . 20
β’ π· = ((π Γ π) β I ) |
79 | | difss 4096 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π Γ π) β I ) β (π Γ π) |
80 | 78, 79 | eqsstri 3983 |
. . . . . . . . . . . . . . . . . . 19
β’ π· β (π Γ π) |
81 | 77, 80 | sstrdi 3961 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (π Γ π)) |
82 | 81 | ssbrd 5153 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πππ β π(π Γ π)π)) |
83 | 82 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πππ) β π(π Γ π)π) |
84 | | brxp 5686 |
. . . . . . . . . . . . . . . 16
β’ (π(π Γ π)π β (π β π β§ π β π)) |
85 | 83, 84 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πππ) β (π β π β§ π β π)) |
86 | 85 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ πππ) β π β π) |
87 | 75, 86 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((π β§ πππ) β (π»βπ) β πΈ) |
88 | | fvco3 6945 |
. . . . . . . . . . . . 13
β’ ((π :πΈβΆπΈ β§ (π»βπ) β πΈ) β ((π β π )β(π»βπ)) = (πβ(π β(π»βπ)))) |
89 | 73, 87, 88 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ πππ) β ((π β π )β(π»βπ)) = (πβ(π β(π»βπ)))) |
90 | 89 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ πππ) β (πβ((π β π )β(π»βπ))) = (πβ(πβ(π β(π»βπ))))) |
91 | 6 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ πππ) β π β mFS) |
92 | 29 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ πππ) β π β ran πΏ) |
93 | 73, 87 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ ((π β§ πππ) β (π β(π»βπ)) β πΈ) |
94 | 2, 3, 28, 27 | msubvrs 34194 |
. . . . . . . . . . . 12
β’ ((π β mFS β§ π β ran πΏ β§ (π β(π»βπ)) β πΈ) β (πβ(πβ(π β(π»βπ)))) = βͺ
π’ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ’)))) |
95 | 91, 92, 93, 94 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ πππ) β (πβ(πβ(π β(π»βπ)))) = βͺ
π’ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ’)))) |
96 | 90, 95 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ πππ) β (πβ((π β π )β(π»βπ))) = βͺ
π’ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ’)))) |
97 | 96 | eleq2d 2824 |
. . . . . . . . 9
β’ ((π β§ πππ) β (π β (πβ((π β π )β(π»βπ))) β π β βͺ
π’ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ’))))) |
98 | | eliun 4963 |
. . . . . . . . 9
β’ (π β βͺ π’ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ’))) β βπ’ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ’)))) |
99 | 97, 98 | bitrdi 287 |
. . . . . . . 8
β’ ((π β§ πππ) β (π β (πβ((π β π )β(π»βπ))) β βπ’ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ’))))) |
100 | 85 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((π β§ πππ) β π β π) |
101 | 75, 100 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((π β§ πππ) β (π»βπ) β πΈ) |
102 | | fvco3 6945 |
. . . . . . . . . . . . 13
β’ ((π :πΈβΆπΈ β§ (π»βπ) β πΈ) β ((π β π )β(π»βπ)) = (πβ(π β(π»βπ)))) |
103 | 73, 101, 102 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ πππ) β ((π β π )β(π»βπ)) = (πβ(π β(π»βπ)))) |
104 | 103 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ πππ) β (πβ((π β π )β(π»βπ))) = (πβ(πβ(π β(π»βπ))))) |
105 | 73, 101 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ ((π β§ πππ) β (π β(π»βπ)) β πΈ) |
106 | 2, 3, 28, 27 | msubvrs 34194 |
. . . . . . . . . . . 12
β’ ((π β mFS β§ π β ran πΏ β§ (π β(π»βπ)) β πΈ) β (πβ(πβ(π β(π»βπ)))) = βͺ
π£ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ£)))) |
107 | 91, 92, 105, 106 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ πππ) β (πβ(πβ(π β(π»βπ)))) = βͺ
π£ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ£)))) |
108 | 104, 107 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ πππ) β (πβ((π β π )β(π»βπ))) = βͺ
π£ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ£)))) |
109 | 108 | eleq2d 2824 |
. . . . . . . . 9
β’ ((π β§ πππ) β (π β (πβ((π β π )β(π»βπ))) β π β βͺ
π£ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ£))))) |
110 | | eliun 4963 |
. . . . . . . . 9
β’ (π β βͺ π£ β (πβ(π β(π»βπ)))(πβ(πβ(π»βπ£))) β βπ£ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ£)))) |
111 | 109, 110 | bitrdi 287 |
. . . . . . . 8
β’ ((π β§ πππ) β (π β (πβ((π β π )β(π»βπ))) β βπ£ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ£))))) |
112 | 99, 111 | anbi12d 632 |
. . . . . . 7
β’ ((π β§ πππ) β ((π β (πβ((π β π )β(π»βπ))) β§ π β (πβ((π β π )β(π»βπ)))) β (βπ’ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ’))) β§ βπ£ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ£)))))) |
113 | | reeanv 3220 |
. . . . . . . 8
β’
(βπ’ β
(πβ(π β(π»βπ)))βπ£ β (πβ(π β(π»βπ)))(π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£)))) β (βπ’ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ’))) β§ βπ£ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ£))))) |
114 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ πππ) β§ (π’ β (πβ(π β(π»βπ))) β§ π£ β (πβ(π β(π»βπ))))) β π) |
115 | | brxp 5686 |
. . . . . . . . . . . 12
β’ (π’((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ))))π£ β (π’ β (πβ(π β(π»βπ))) β§ π£ β (πβ(π β(π»βπ))))) |
116 | | mclsppslem.12 |
. . . . . . . . . . . . . . 15
β’ (π β βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) |
117 | | breq12 5115 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ = π β§ π€ = π) β (π§ππ€ β πππ)) |
118 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π§ = π β§ π€ = π) β π§ = π) |
119 | 118 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π§ = π β§ π€ = π) β (π»βπ§) = (π»βπ)) |
120 | 119 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π§ = π β§ π€ = π) β (π β(π»βπ§)) = (π β(π»βπ))) |
121 | 120 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π§ = π β§ π€ = π) β (πβ(π β(π»βπ§))) = (πβ(π β(π»βπ)))) |
122 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π§ = π β§ π€ = π) β π€ = π) |
123 | 122 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π§ = π β§ π€ = π) β (π»βπ€) = (π»βπ)) |
124 | 123 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π§ = π β§ π€ = π) β (π β(π»βπ€)) = (π β(π»βπ))) |
125 | 124 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π§ = π β§ π€ = π) β (πβ(π β(π»βπ€))) = (πβ(π β(π»βπ)))) |
126 | 121, 125 | xpeq12d 5669 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π§ = π β§ π€ = π) β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) = ((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ))))) |
127 | 126 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ = π β§ π€ = π) β (((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π β ((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ)))) β π)) |
128 | 117, 127 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ = π β§ π€ = π) β ((π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π) β (πππ β ((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ)))) β π))) |
129 | 128 | spc2gv 3562 |
. . . . . . . . . . . . . . . 16
β’ ((π β V β§ π β V) β (βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π) β (πππ β ((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ)))) β π))) |
130 | 129 | el2v 3456 |
. . . . . . . . . . . . . . 15
β’
(βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π) β (πππ β ((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ)))) β π)) |
131 | 116, 130 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (πππ β ((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ)))) β π)) |
132 | 131 | imp 408 |
. . . . . . . . . . . . 13
β’ ((π β§ πππ) β ((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ)))) β π) |
133 | 132 | ssbrd 5153 |
. . . . . . . . . . . 12
β’ ((π β§ πππ) β (π’((πβ(π β(π»βπ))) Γ (πβ(π β(π»βπ))))π£ β π’ππ£)) |
134 | 115, 133 | biimtrrid 242 |
. . . . . . . . . . 11
β’ ((π β§ πππ) β ((π’ β (πβ(π β(π»βπ))) β§ π£ β (πβ(π β(π»βπ)))) β π’ππ£)) |
135 | 134 | imp 408 |
. . . . . . . . . 10
β’ (((π β§ πππ) β§ (π’ β (πβ(π β(π»βπ))) β§ π£ β (πβ(π β(π»βπ))))) β π’ππ£) |
136 | | vex 3452 |
. . . . . . . . . . . . 13
β’ π’ β V |
137 | | vex 3452 |
. . . . . . . . . . . . 13
β’ π£ β V |
138 | | breq12 5115 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π’ β§ π¦ = π£) β (π₯ππ¦ β π’ππ£)) |
139 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ = π’ β§ π¦ = π£) β π₯ = π’) |
140 | 139 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ = π’ β§ π¦ = π£) β (π»βπ₯) = (π»βπ’)) |
141 | 140 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ = π’ β§ π¦ = π£) β (πβ(π»βπ₯)) = (πβ(π»βπ’))) |
142 | 141 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π’ β§ π¦ = π£) β (πβ(πβ(π»βπ₯))) = (πβ(πβ(π»βπ’)))) |
143 | 142 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π’ β§ π¦ = π£) β (π β (πβ(πβ(π»βπ₯))) β π β (πβ(πβ(π»βπ’))))) |
144 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ = π’ β§ π¦ = π£) β π¦ = π£) |
145 | 144 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ = π’ β§ π¦ = π£) β (π»βπ¦) = (π»βπ£)) |
146 | 145 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ = π’ β§ π¦ = π£) β (πβ(π»βπ¦)) = (πβ(π»βπ£))) |
147 | 146 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π’ β§ π¦ = π£) β (πβ(πβ(π»βπ¦))) = (πβ(πβ(π»βπ£)))) |
148 | 147 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π’ β§ π¦ = π£) β (π β (πβ(πβ(π»βπ¦))) β π β (πβ(πβ(π»βπ£))))) |
149 | 138, 143,
148 | 3anbi123d 1437 |
. . . . . . . . . . . . . . 15
β’ ((π₯ = π’ β§ π¦ = π£) β ((π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦)))) β (π’ππ£ β§ π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£)))))) |
150 | 149 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ ((π₯ = π’ β§ π¦ = π£) β ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β (π β§ (π’ππ£ β§ π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£))))))) |
151 | 150 | imbi1d 342 |
. . . . . . . . . . . . 13
β’ ((π₯ = π’ β§ π¦ = π£) β (((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) β ((π β§ (π’ππ£ β§ π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£))))) β ππΎπ))) |
152 | | mclspps.8 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) |
153 | 136, 137,
151, 152 | vtocl2 3523 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ππ£ β§ π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£))))) β ππΎπ) |
154 | 153 | 3exp2 1355 |
. . . . . . . . . . 11
β’ (π β (π’ππ£ β (π β (πβ(πβ(π»βπ’))) β (π β (πβ(πβ(π»βπ£))) β ππΎπ)))) |
155 | 154 | imp4b 423 |
. . . . . . . . . 10
β’ ((π β§ π’ππ£) β ((π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£)))) β ππΎπ)) |
156 | 114, 135,
155 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ πππ) β§ (π’ β (πβ(π β(π»βπ))) β§ π£ β (πβ(π β(π»βπ))))) β ((π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£)))) β ππΎπ)) |
157 | 156 | rexlimdvva 3206 |
. . . . . . . 8
β’ ((π β§ πππ) β (βπ’ β (πβ(π β(π»βπ)))βπ£ β (πβ(π β(π»βπ)))(π β (πβ(πβ(π»βπ’))) β§ π β (πβ(πβ(π»βπ£)))) β ππΎπ)) |
158 | 113, 157 | biimtrrid 242 |
. . . . . . 7
β’ ((π β§ πππ) β ((βπ’ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ’))) β§ βπ£ β (πβ(π β(π»βπ)))π β (πβ(πβ(π»βπ£)))) β ππΎπ)) |
159 | 112, 158 | sylbid 239 |
. . . . . 6
β’ ((π β§ πππ) β ((π β (πβ((π β π )β(π»βπ))) β§ π β (πβ((π β π )β(π»βπ)))) β ππΎπ)) |
160 | 159 | exp4b 432 |
. . . . 5
β’ (π β (πππ β (π β (πβ((π β π )β(π»βπ))) β (π β (πβ((π β π )β(π»βπ))) β ππΎπ)))) |
161 | 160 | 3imp2 1350 |
. . . 4
β’ ((π β§ (πππ β§ π β (πβ((π β π )β(π»βπ))) β§ π β (πβ((π β π )β(π»βπ))))) β ππΎπ) |
162 | 16, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161 | mclsax 34203 |
. . 3
β’ (π β ((π β π )βπ) β (πΎπΆπ΅)) |
163 | 22, 162 | eqeltrrd 2839 |
. 2
β’ (π β (πβ(π βπ)) β (πΎπΆπ΅)) |
164 | 33 | ffnd 6674 |
. . 3
β’ (π β π Fn πΈ) |
165 | | elpreima 7013 |
. . 3
β’ (π Fn πΈ β ((π βπ) β (β‘π β (πΎπΆπ΅)) β ((π βπ) β πΈ β§ (πβ(π βπ)) β (πΎπΆπ΅)))) |
166 | 164, 165 | syl 17 |
. 2
β’ (π β ((π βπ) β (β‘π β (πΎπΆπ΅)) β ((π βπ) β πΈ β§ (πβ(π βπ)) β (πΎπΆπ΅)))) |
167 | 20, 163, 166 | mpbir2and 712 |
1
β’ (π β (π βπ) β (β‘π β (πΎπΆπ΅))) |