Step | Hyp | Ref
| Expression |
1 | | simp2 1136 |
. . . 4
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β π β π΄) |
2 | | ipodrscl 18496 |
. . . . . 6
β’
((toIncβπ΄)
β Dirset β π΄
β V) |
3 | | eqid 2731 |
. . . . . . 7
β’
(toIncβπ΄) =
(toIncβπ΄) |
4 | 3 | ipobas 18489 |
. . . . . 6
β’ (π΄ β V β π΄ =
(Baseβ(toIncβπ΄))) |
5 | 2, 4 | syl 17 |
. . . . 5
β’
((toIncβπ΄)
β Dirset β π΄ =
(Baseβ(toIncβπ΄))) |
6 | 5 | 3ad2ant1 1132 |
. . . 4
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β π΄ =
(Baseβ(toIncβπ΄))) |
7 | 1, 6 | sseqtrd 4022 |
. . 3
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β π β
(Baseβ(toIncβπ΄))) |
8 | | eqid 2731 |
. . . 4
β’
(Baseβ(toIncβπ΄)) = (Baseβ(toIncβπ΄)) |
9 | | eqid 2731 |
. . . 4
β’
(leβ(toIncβπ΄)) = (leβ(toIncβπ΄)) |
10 | 8, 9 | drsdirfi 18263 |
. . 3
β’
(((toIncβπ΄)
β Dirset β§ π
β (Baseβ(toIncβπ΄)) β§ π β Fin) β βπ§ β
(Baseβ(toIncβπ΄))βπ€ β π π€(leβ(toIncβπ΄))π§) |
11 | 7, 10 | syld3an2 1410 |
. 2
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β βπ§ β
(Baseβ(toIncβπ΄))βπ€ β π π€(leβ(toIncβπ΄))π§) |
12 | 6 | rexeqdv 3325 |
. . 3
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β
(βπ§ β π΄ βπ€ β π π€(leβ(toIncβπ΄))π§ β βπ§ β (Baseβ(toIncβπ΄))βπ€ β π π€(leβ(toIncβπ΄))π§)) |
13 | 2 | 3ad2ant1 1132 |
. . . . . . . . 9
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β π΄ β V) |
14 | 13 | adantr 480 |
. . . . . . . 8
β’
((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ (π§ β π΄ β§ π€ β π)) β π΄ β V) |
15 | 1 | sselda 3982 |
. . . . . . . . 9
β’
((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ π€ β π) β π€ β π΄) |
16 | 15 | adantrl 713 |
. . . . . . . 8
β’
((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ (π§ β π΄ β§ π€ β π)) β π€ β π΄) |
17 | | simprl 768 |
. . . . . . . 8
β’
((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ (π§ β π΄ β§ π€ β π)) β π§ β π΄) |
18 | 3, 9 | ipole 18492 |
. . . . . . . 8
β’ ((π΄ β V β§ π€ β π΄ β§ π§ β π΄) β (π€(leβ(toIncβπ΄))π§ β π€ β π§)) |
19 | 14, 16, 17, 18 | syl3anc 1370 |
. . . . . . 7
β’
((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ (π§ β π΄ β§ π€ β π)) β (π€(leβ(toIncβπ΄))π§ β π€ β π§)) |
20 | 19 | anassrs 467 |
. . . . . 6
β’
(((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ π§ β π΄) β§ π€ β π) β (π€(leβ(toIncβπ΄))π§ β π€ β π§)) |
21 | 20 | ralbidva 3174 |
. . . . 5
β’
((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ π§ β π΄) β (βπ€ β π π€(leβ(toIncβπ΄))π§ β βπ€ β π π€ β π§)) |
22 | | unissb 4943 |
. . . . 5
β’ (βͺ π
β π§ β
βπ€ β π π€ β π§) |
23 | 21, 22 | bitr4di 289 |
. . . 4
β’
((((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β§ π§ β π΄) β (βπ€ β π π€(leβ(toIncβπ΄))π§ β βͺ π β π§)) |
24 | 23 | rexbidva 3175 |
. . 3
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β
(βπ§ β π΄ βπ€ β π π€(leβ(toIncβπ΄))π§ β βπ§ β π΄ βͺ π β π§)) |
25 | 12, 24 | bitr3d 281 |
. 2
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β
(βπ§ β
(Baseβ(toIncβπ΄))βπ€ β π π€(leβ(toIncβπ΄))π§ β βπ§ β π΄ βͺ π β π§)) |
26 | 11, 25 | mpbid 231 |
1
β’
(((toIncβπ΄)
β Dirset β§ π
β π΄ β§ π β Fin) β βπ§ β π΄ βͺ π β π§) |