Step | Hyp | Ref
| Expression |
1 | | isucn2.1 |
. . 3
β’ (π β π β (UnifOnβπ)) |
2 | | isucn2.2 |
. . 3
β’ (π β π β (UnifOnβπ)) |
3 | | isucn 23646 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))))) |
4 | 1, 2, 3 | syl2anc 585 |
. 2
β’ (π β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))))) |
5 | | breq 5112 |
. . . . . . . . . 10
β’ (π£ = π β ((πΉβπ₯)π£(πΉβπ¦) β (πΉβπ₯)π (πΉβπ¦))) |
6 | 5 | imbi2d 341 |
. . . . . . . . 9
β’ (π£ = π β ((π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)) β (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
7 | 6 | ralbidv 3175 |
. . . . . . . 8
β’ (π£ = π β (βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)) β βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
8 | 7 | rexralbidv 3215 |
. . . . . . 7
β’ (π£ = π β (βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
9 | | simplr 768 |
. . . . . . 7
β’ ((((π β§ πΉ:πβΆπ) β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β§ π β π) β βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) |
10 | | isucn2.4 |
. . . . . . . . . . . 12
β’ (π β π β (fBasβ(π Γ π))) |
11 | | ssfg 23239 |
. . . . . . . . . . . 12
β’ (π β (fBasβ(π Γ π)) β π β ((π Γ π)filGenπ)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β ((π Γ π)filGenπ)) |
13 | | isucn2.v |
. . . . . . . . . . 11
β’ π = ((π Γ π)filGenπ) |
14 | 12, 13 | sseqtrrdi 4000 |
. . . . . . . . . 10
β’ (π β π β π) |
15 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΉ:πβΆπ) β π β π) |
16 | 15 | adantr 482 |
. . . . . . . 8
β’ (((π β§ πΉ:πβΆπ) β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β π β π) |
17 | 16 | sselda 3949 |
. . . . . . 7
β’ ((((π β§ πΉ:πβΆπ) β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β§ π β π) β π β π) |
18 | 8, 9, 17 | rspcdva 3585 |
. . . . . 6
β’ ((((π β§ πΉ:πβΆπ) β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β§ π β π) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) |
19 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π) β π’ β π) |
20 | | isucn2.u |
. . . . . . . . . . . 12
β’ π = ((π Γ π)filGenπ
) |
21 | 19, 20 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ ((π β§ π’ β π) β π’ β ((π Γ π)filGenπ
)) |
22 | | isucn2.3 |
. . . . . . . . . . . . 13
β’ (π β π
β (fBasβ(π Γ π))) |
23 | | elfg 23238 |
. . . . . . . . . . . . 13
β’ (π
β (fBasβ(π Γ π)) β (π’ β ((π Γ π)filGenπ
) β (π’ β (π Γ π) β§ βπ β π
π β π’))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π’ β ((π Γ π)filGenπ
) β (π’ β (π Γ π) β§ βπ β π
π β π’))) |
25 | 24 | simplbda 501 |
. . . . . . . . . . 11
β’ ((π β§ π’ β ((π Γ π)filGenπ
)) β βπ β π
π β π’) |
26 | 21, 25 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π’ β π) β βπ β π
π β π’) |
27 | | ssbr 5154 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π’ β (π₯ππ¦ β π₯π’π¦)) |
28 | 27 | imim1d 82 |
. . . . . . . . . . . . . . . . 17
β’ (π β π’ β ((π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π
) β§ π β π’) β ((π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
30 | 29 | ralrimivw 3148 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π
) β§ π β π’) β βπ¦ β π ((π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
31 | 30 | ralrimivw 3148 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π
) β§ π β π’) β βπ₯ β π βπ¦ β π ((π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
32 | | ralim 3090 |
. . . . . . . . . . . . . . 15
β’
(βπ¦ β
π ((π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))) β (βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
33 | 32 | ralimi 3087 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
π βπ¦ β π ((π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))) β βπ₯ β π (βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
34 | | ralim 3090 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
π (βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))) β (βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
35 | 31, 33, 34 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π
) β§ π β π’) β (βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
36 | 35 | ex 414 |
. . . . . . . . . . . 12
β’ ((π β§ π β π
) β (π β π’ β (βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))))) |
37 | 36 | reximdva 3166 |
. . . . . . . . . . 11
β’ (π β (βπ β π
π β π’ β βπ β π
(βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))))) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π’ β π) β (βπ β π
π β π’ β βπ β π
(βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))))) |
39 | 26, 38 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π’ β π) β βπ β π
(βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
40 | | r19.37v 3179 |
. . . . . . . . 9
β’
(βπ β
π
(βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))) β (βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
β’ ((π β§ π’ β π) β (βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
42 | 41 | rexlimdva 3153 |
. . . . . . 7
β’ (π β (βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
43 | 42 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ πΉ:πβΆπ) β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β§ π β π) β (βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
44 | 18, 43 | mpd 15 |
. . . . 5
β’ ((((π β§ πΉ:πβΆπ) β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β§ π β π) β βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))) |
45 | 44 | ralrimiva 3144 |
. . . 4
β’ (((π β§ πΉ:πβΆπ) β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))) |
46 | | ssfg 23239 |
. . . . . . . . . . 11
β’ (π
β (fBasβ(π Γ π)) β π
β ((π Γ π)filGenπ
)) |
47 | 22, 46 | syl 17 |
. . . . . . . . . 10
β’ (π β π
β ((π Γ π)filGenπ
)) |
48 | 47, 20 | sseqtrrdi 4000 |
. . . . . . . . 9
β’ (π β π
β π) |
49 | | ssrexv 4016 |
. . . . . . . . . 10
β’ (π
β π β (βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
50 | | breq 5112 |
. . . . . . . . . . . . 13
β’ (π = π’ β (π₯ππ¦ β π₯π’π¦)) |
51 | 50 | imbi1d 342 |
. . . . . . . . . . . 12
β’ (π = π’ β ((π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
52 | 51 | 2ralbidv 3213 |
. . . . . . . . . . 11
β’ (π = π’ β (βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
53 | 52 | cbvrexvw 3229 |
. . . . . . . . . 10
β’
(βπ β
π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) |
54 | 49, 53 | syl6ib 251 |
. . . . . . . . 9
β’ (π
β π β (βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
55 | 48, 54 | syl 17 |
. . . . . . . 8
β’ (π β (βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
56 | 55 | ralimdv 3167 |
. . . . . . 7
β’ (π β (βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
57 | 56 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ:πβΆπ) β (βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)))) |
58 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π (π β§ πΉ:πβΆπ) |
59 | | nfra1 3270 |
. . . . . . . . . . 11
β’
β²π βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) |
60 | 58, 59 | nfan 1903 |
. . . . . . . . . 10
β’
β²π ((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) |
61 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π£ β π |
62 | 60, 61 | nfan 1903 |
. . . . . . . . 9
β’
β²π (((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) |
63 | | rspa 3234 |
. . . . . . . . . . 11
β’
((βπ β
π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β§ π β π) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) |
64 | 63 | ad5ant24 760 |
. . . . . . . . . 10
β’
((((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β§ π β π) β§ π β π£) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) |
65 | | simp-4l 782 |
. . . . . . . . . . 11
β’
((((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β§ π β π) β§ π β π£) β (π β§ πΉ:πβΆπ)) |
66 | | simplr 768 |
. . . . . . . . . . 11
β’
((((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β§ π β π) β§ π β π£) β π β π) |
67 | | simpr 486 |
. . . . . . . . . . 11
β’
((((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β§ π β π) β§ π β π£) β π β π£) |
68 | | ssbr 5154 |
. . . . . . . . . . . . . . . 16
β’ (π β π£ β ((πΉβπ₯)π (πΉβπ¦) β (πΉβπ₯)π£(πΉβπ¦))) |
69 | 68 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΉ:πβΆπ) β§ π β π) β§ π β π£) β ((πΉβπ₯)π (πΉβπ¦) β (πΉβπ₯)π£(πΉβπ¦))) |
70 | 69 | imim2d 57 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΉ:πβΆπ) β§ π β π) β§ π β π£) β ((π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)))) |
71 | 70 | ralimdv 3167 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΉ:πβΆπ) β§ π β π) β§ π β π£) β (βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)))) |
72 | 71 | ralimdv 3167 |
. . . . . . . . . . . 12
β’ ((((π β§ πΉ:πβΆπ) β§ π β π) β§ π β π£) β (βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)))) |
73 | 72 | reximdv 3168 |
. . . . . . . . . . 11
β’ ((((π β§ πΉ:πβΆπ) β§ π β π) β§ π β π£) β (βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)))) |
74 | 65, 66, 67, 73 | syl21anc 837 |
. . . . . . . . . 10
β’
((((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β§ π β π) β§ π β π£) β (βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)))) |
75 | 64, 74 | mpd 15 |
. . . . . . . . 9
β’
((((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β§ π β π) β§ π β π£) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) |
76 | 10 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β π β (fBasβ(π Γ π))) |
77 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β π£ β π) |
78 | 77, 13 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ ((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β π£ β ((π Γ π)filGenπ)) |
79 | | elfg 23238 |
. . . . . . . . . . 11
β’ (π β (fBasβ(π Γ π)) β (π£ β ((π Γ π)filGenπ) β (π£ β (π Γ π) β§ βπ β π π β π£))) |
80 | 79 | simplbda 501 |
. . . . . . . . . 10
β’ ((π β (fBasβ(π Γ π)) β§ π£ β ((π Γ π)filGenπ)) β βπ β π π β π£) |
81 | 76, 78, 80 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β βπ β π π β π£) |
82 | 62, 75, 81 | r19.29af 3254 |
. . . . . . . 8
β’ ((((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β§ π£ β π) β βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) |
83 | 82 | ralrimiva 3144 |
. . . . . . 7
β’ (((π β§ πΉ:πβΆπ) β§ βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦))) β βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) |
84 | 83 | ex 414 |
. . . . . 6
β’ ((π β§ πΉ:πβΆπ) β (βπ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)))) |
85 | 57, 84 | syld 47 |
. . . . 5
β’ ((π β§ πΉ:πβΆπ) β (βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)) β βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)))) |
86 | 85 | imp 408 |
. . . 4
β’ (((π β§ πΉ:πβΆπ) β§ βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))) β βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) |
87 | 45, 86 | impbida 800 |
. . 3
β’ ((π β§ πΉ:πβΆπ) β (βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦)) β βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦)))) |
88 | 87 | pm5.32da 580 |
. 2
β’ (π β ((πΉ:πβΆπ β§ βπ£ β π βπ’ β π βπ₯ β π βπ¦ β π (π₯π’π¦ β (πΉβπ₯)π£(πΉβπ¦))) β (πΉ:πβΆπ β§ βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))))) |
89 | 4, 88 | bitrd 279 |
1
β’ (π β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ β π βπ β π
βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))))) |