Step | Hyp | Ref
| Expression |
1 | | ovexd 7393 |
. . 3
β’ ((πΎ β Proset β§ π΄ β π΅) β (πΎ βΎs π΄) β V) |
2 | | simp-4l 782 |
. . . . . . . 8
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β πΎ β Proset ) |
3 | | simp-4r 783 |
. . . . . . . . 9
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β π΄ β π΅) |
4 | | simpllr 775 |
. . . . . . . . 9
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β π₯ β π΄) |
5 | 3, 4 | sseldd 3946 |
. . . . . . . 8
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β π₯ β π΅) |
6 | 2, 5 | jca 513 |
. . . . . . 7
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β (πΎ β Proset β§ π₯ β π΅)) |
7 | | simplr 768 |
. . . . . . . 8
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β π¦ β π΄) |
8 | 3, 7 | sseldd 3946 |
. . . . . . 7
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β π¦ β π΅) |
9 | | simpr 486 |
. . . . . . . 8
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β π§ β π΄) |
10 | 3, 9 | sseldd 3946 |
. . . . . . 7
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β π§ β π΅) |
11 | | ressprs.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΎ) |
12 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(leβπΎ) =
(leβπΎ) |
13 | 11, 12 | isprs 18191 |
. . . . . . . . . . 11
β’ (πΎ β Proset β (πΎ β V β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
14 | 13 | simprbi 498 |
. . . . . . . . . 10
β’ (πΎ β Proset β
βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
15 | 14 | r19.21bi 3233 |
. . . . . . . . 9
β’ ((πΎ β Proset β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
16 | 15 | r19.21bi 3233 |
. . . . . . . 8
β’ (((πΎ β Proset β§ π₯ β π΅) β§ π¦ β π΅) β βπ§ β π΅ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
17 | 16 | r19.21bi 3233 |
. . . . . . 7
β’ ((((πΎ β Proset β§ π₯ β π΅) β§ π¦ β π΅) β§ π§ β π΅) β (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
18 | 6, 8, 10, 17 | syl21anc 837 |
. . . . . 6
β’
(((((πΎ β Proset
β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β§ π§ β π΄) β (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
19 | 18 | ralrimiva 3140 |
. . . . 5
β’ ((((πΎ β Proset β§ π΄ β π΅) β§ π₯ β π΄) β§ π¦ β π΄) β βπ§ β π΄ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
20 | 19 | ralrimiva 3140 |
. . . 4
β’ (((πΎ β Proset β§ π΄ β π΅) β§ π₯ β π΄) β βπ¦ β π΄ βπ§ β π΄ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
21 | 20 | ralrimiva 3140 |
. . 3
β’ ((πΎ β Proset β§ π΄ β π΅) β βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
22 | | eqid 2733 |
. . . . . . 7
β’ (πΎ βΎs π΄) = (πΎ βΎs π΄) |
23 | 22, 11 | ressbas2 17125 |
. . . . . 6
β’ (π΄ β π΅ β π΄ = (Baseβ(πΎ βΎs π΄))) |
24 | 23 | adantl 483 |
. . . . 5
β’ ((πΎ β Proset β§ π΄ β π΅) β π΄ = (Baseβ(πΎ βΎs π΄))) |
25 | 11 | fvexi 6857 |
. . . . . . . . . . . 12
β’ π΅ β V |
26 | 25 | ssex 5279 |
. . . . . . . . . . 11
β’ (π΄ β π΅ β π΄ β V) |
27 | 22, 12 | ressle 17266 |
. . . . . . . . . . 11
β’ (π΄ β V β (leβπΎ) = (leβ(πΎ βΎs π΄))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
β’ (π΄ β π΅ β (leβπΎ) = (leβ(πΎ βΎs π΄))) |
29 | 28 | adantl 483 |
. . . . . . . . 9
β’ ((πΎ β Proset β§ π΄ β π΅) β (leβπΎ) = (leβ(πΎ βΎs π΄))) |
30 | 29 | breqd 5117 |
. . . . . . . 8
β’ ((πΎ β Proset β§ π΄ β π΅) β (π₯(leβπΎ)π₯ β π₯(leβ(πΎ βΎs π΄))π₯)) |
31 | 29 | breqd 5117 |
. . . . . . . . . 10
β’ ((πΎ β Proset β§ π΄ β π΅) β (π₯(leβπΎ)π¦ β π₯(leβ(πΎ βΎs π΄))π¦)) |
32 | 29 | breqd 5117 |
. . . . . . . . . 10
β’ ((πΎ β Proset β§ π΄ β π΅) β (π¦(leβπΎ)π§ β π¦(leβ(πΎ βΎs π΄))π§)) |
33 | 31, 32 | anbi12d 632 |
. . . . . . . . 9
β’ ((πΎ β Proset β§ π΄ β π΅) β ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β (π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§))) |
34 | 29 | breqd 5117 |
. . . . . . . . 9
β’ ((πΎ β Proset β§ π΄ β π΅) β (π₯(leβπΎ)π§ β π₯(leβ(πΎ βΎs π΄))π§)) |
35 | 33, 34 | imbi12d 345 |
. . . . . . . 8
β’ ((πΎ β Proset β§ π΄ β π΅) β (((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§) β ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§))) |
36 | 30, 35 | anbi12d 632 |
. . . . . . 7
β’ ((πΎ β Proset β§ π΄ β π΅) β ((π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)) β (π₯(leβ(πΎ βΎs π΄))π₯ β§ ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§)))) |
37 | 24, 36 | raleqbidv 3318 |
. . . . . 6
β’ ((πΎ β Proset β§ π΄ β π΅) β (βπ§ β π΄ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)) β βπ§ β (Baseβ(πΎ βΎs π΄))(π₯(leβ(πΎ βΎs π΄))π₯ β§ ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§)))) |
38 | 24, 37 | raleqbidv 3318 |
. . . . 5
β’ ((πΎ β Proset β§ π΄ β π΅) β (βπ¦ β π΄ βπ§ β π΄ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)) β βπ¦ β (Baseβ(πΎ βΎs π΄))βπ§ β (Baseβ(πΎ βΎs π΄))(π₯(leβ(πΎ βΎs π΄))π₯ β§ ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§)))) |
39 | 24, 38 | raleqbidv 3318 |
. . . 4
β’ ((πΎ β Proset β§ π΄ β π΅) β (βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)) β βπ₯ β (Baseβ(πΎ βΎs π΄))βπ¦ β (Baseβ(πΎ βΎs π΄))βπ§ β (Baseβ(πΎ βΎs π΄))(π₯(leβ(πΎ βΎs π΄))π₯ β§ ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§)))) |
40 | 39 | anbi2d 630 |
. . 3
β’ ((πΎ β Proset β§ π΄ β π΅) β (((πΎ βΎs π΄) β V β§ βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) β ((πΎ βΎs π΄) β V β§ βπ₯ β (Baseβ(πΎ βΎs π΄))βπ¦ β (Baseβ(πΎ βΎs π΄))βπ§ β (Baseβ(πΎ βΎs π΄))(π₯(leβ(πΎ βΎs π΄))π₯ β§ ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§))))) |
41 | 1, 21, 40 | mpbi2and 711 |
. 2
β’ ((πΎ β Proset β§ π΄ β π΅) β ((πΎ βΎs π΄) β V β§ βπ₯ β (Baseβ(πΎ βΎs π΄))βπ¦ β (Baseβ(πΎ βΎs π΄))βπ§ β (Baseβ(πΎ βΎs π΄))(π₯(leβ(πΎ βΎs π΄))π₯ β§ ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§)))) |
42 | | eqid 2733 |
. . 3
β’
(Baseβ(πΎ
βΎs π΄)) =
(Baseβ(πΎ
βΎs π΄)) |
43 | | eqid 2733 |
. . 3
β’
(leβ(πΎ
βΎs π΄)) =
(leβ(πΎ
βΎs π΄)) |
44 | 42, 43 | isprs 18191 |
. 2
β’ ((πΎ βΎs π΄) β Proset β ((πΎ βΎs π΄) β V β§ βπ₯ β (Baseβ(πΎ βΎs π΄))βπ¦ β (Baseβ(πΎ βΎs π΄))βπ§ β (Baseβ(πΎ βΎs π΄))(π₯(leβ(πΎ βΎs π΄))π₯ β§ ((π₯(leβ(πΎ βΎs π΄))π¦ β§ π¦(leβ(πΎ βΎs π΄))π§) β π₯(leβ(πΎ βΎs π΄))π§)))) |
45 | 41, 44 | sylibr 233 |
1
β’ ((πΎ β Proset β§ π΄ β π΅) β (πΎ βΎs π΄) β Proset ) |