Step | Hyp | Ref
| Expression |
1 | | ipodrsima.a |
. . 3
β’ (π β (πΉ β π΅) β π) |
2 | 1 | elexd 3494 |
. 2
β’ (π β (πΉ β π΅) β V) |
3 | | ipodrsima.d |
. . . . 5
β’ (π β (toIncβπ΅) β
Dirset) |
4 | | isipodrs 18495 |
. . . . 5
β’
((toIncβπ΅)
β Dirset β (π΅
β V β§ π΅ β
β
β§ βπ
β π΅ βπ β π΅ βπ β π΅ (π βͺ π) β π)) |
5 | 3, 4 | sylib 217 |
. . . 4
β’ (π β (π΅ β V β§ π΅ β β
β§ βπ β π΅ βπ β π΅ βπ β π΅ (π βͺ π) β π)) |
6 | 5 | simp2d 1142 |
. . 3
β’ (π β π΅ β β
) |
7 | | ipodrsima.f |
. . . . 5
β’ (π β πΉ Fn π« π΄) |
8 | | ipodrsima.s |
. . . . 5
β’ (π β π΅ β π« π΄) |
9 | | fnimaeq0 6683 |
. . . . 5
β’ ((πΉ Fn π« π΄ β§ π΅ β π« π΄) β ((πΉ β π΅) = β
β π΅ = β
)) |
10 | 7, 8, 9 | syl2anc 583 |
. . . 4
β’ (π β ((πΉ β π΅) = β
β π΅ = β
)) |
11 | 10 | necon3bid 2984 |
. . 3
β’ (π β ((πΉ β π΅) β β
β π΅ β β
)) |
12 | 6, 11 | mpbird 257 |
. 2
β’ (π β (πΉ β π΅) β β
) |
13 | 5 | simp3d 1143 |
. . . 4
β’ (π β βπ β π΅ βπ β π΅ βπ β π΅ (π βͺ π) β π) |
14 | | simplll 772 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β π) |
15 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β π β π) |
16 | 8 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β π΅ β π« π΄) |
17 | | simprr 770 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β π β π΅) |
18 | 16, 17 | sseldd 3983 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β π β π« π΄) |
19 | 18 | elpwid 4611 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β π β π΄) |
20 | 19 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β π β π΄) |
21 | | vex 3477 |
. . . . . . . . . . . . 13
β’ π β V |
22 | | vex 3477 |
. . . . . . . . . . . . 13
β’ π β V |
23 | | sseq12 4009 |
. . . . . . . . . . . . . . . 16
β’ ((π’ = π β§ π£ = π) β (π’ β π£ β π β π)) |
24 | | sseq1 4007 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = π β (π£ β π΄ β π β π΄)) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((π’ = π β§ π£ = π) β (π£ β π΄ β π β π΄)) |
26 | 23, 25 | anbi12d 630 |
. . . . . . . . . . . . . . 15
β’ ((π’ = π β§ π£ = π) β ((π’ β π£ β§ π£ β π΄) β (π β π β§ π β π΄))) |
27 | 26 | anbi2d 628 |
. . . . . . . . . . . . . 14
β’ ((π’ = π β§ π£ = π) β ((π β§ (π’ β π£ β§ π£ β π΄)) β (π β§ (π β π β§ π β π΄)))) |
28 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π’ = π β (πΉβπ’) = (πΉβπ)) |
29 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π£ = π β (πΉβπ£) = (πΉβπ)) |
30 | | sseq12 4009 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ’) = (πΉβπ) β§ (πΉβπ£) = (πΉβπ)) β ((πΉβπ’) β (πΉβπ£) β (πΉβπ) β (πΉβπ))) |
31 | 28, 29, 30 | syl2an 595 |
. . . . . . . . . . . . . 14
β’ ((π’ = π β§ π£ = π) β ((πΉβπ’) β (πΉβπ£) β (πΉβπ) β (πΉβπ))) |
32 | 27, 31 | imbi12d 344 |
. . . . . . . . . . . . 13
β’ ((π’ = π β§ π£ = π) β (((π β§ (π’ β π£ β§ π£ β π΄)) β (πΉβπ’) β (πΉβπ£)) β ((π β§ (π β π β§ π β π΄)) β (πΉβπ) β (πΉβπ)))) |
33 | | ipodrsima.m |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β π£ β§ π£ β π΄)) β (πΉβπ’) β (πΉβπ£)) |
34 | 21, 22, 32, 33 | vtocl2 3554 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π β π΄)) β (πΉβπ) β (πΉβπ)) |
35 | 14, 15, 20, 34 | syl12anc 834 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β (πΉβπ) β (πΉβπ)) |
36 | 35 | ex 412 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β (π β π β (πΉβπ) β (πΉβπ))) |
37 | | simplll 772 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β π) |
38 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β π β π) |
39 | 19 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β π β π΄) |
40 | | vex 3477 |
. . . . . . . . . . . . 13
β’ π β V |
41 | | sseq12 4009 |
. . . . . . . . . . . . . . . 16
β’ ((π’ = π β§ π£ = π) β (π’ β π£ β π β π)) |
42 | 24 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((π’ = π β§ π£ = π) β (π£ β π΄ β π β π΄)) |
43 | 41, 42 | anbi12d 630 |
. . . . . . . . . . . . . . 15
β’ ((π’ = π β§ π£ = π) β ((π’ β π£ β§ π£ β π΄) β (π β π β§ π β π΄))) |
44 | 43 | anbi2d 628 |
. . . . . . . . . . . . . 14
β’ ((π’ = π β§ π£ = π) β ((π β§ (π’ β π£ β§ π£ β π΄)) β (π β§ (π β π β§ π β π΄)))) |
45 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π’ = π β (πΉβπ’) = (πΉβπ)) |
46 | | sseq12 4009 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ’) = (πΉβπ) β§ (πΉβπ£) = (πΉβπ)) β ((πΉβπ’) β (πΉβπ£) β (πΉβπ) β (πΉβπ))) |
47 | 45, 29, 46 | syl2an 595 |
. . . . . . . . . . . . . 14
β’ ((π’ = π β§ π£ = π) β ((πΉβπ’) β (πΉβπ£) β (πΉβπ) β (πΉβπ))) |
48 | 44, 47 | imbi12d 344 |
. . . . . . . . . . . . 13
β’ ((π’ = π β§ π£ = π) β (((π β§ (π’ β π£ β§ π£ β π΄)) β (πΉβπ’) β (πΉβπ£)) β ((π β§ (π β π β§ π β π΄)) β (πΉβπ) β (πΉβπ)))) |
49 | 40, 22, 48, 33 | vtocl2 3554 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π β π΄)) β (πΉβπ) β (πΉβπ)) |
50 | 37, 38, 39, 49 | syl12anc 834 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β§ π β π) β (πΉβπ) β (πΉβπ)) |
51 | 50 | ex 412 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β (π β π β (πΉβπ) β (πΉβπ))) |
52 | 36, 51 | anim12d 608 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π β π β§ π β π) β ((πΉβπ) β (πΉβπ) β§ (πΉβπ) β (πΉβπ)))) |
53 | | unss 4184 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (π βͺ π) β π) |
54 | | unss 4184 |
. . . . . . . . 9
β’ (((πΉβπ) β (πΉβπ) β§ (πΉβπ) β (πΉβπ)) β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
55 | 52, 53, 54 | 3imtr3g 295 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π βͺ π) β π β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
56 | 55 | anassrs 467 |
. . . . . . 7
β’ ((((π β§ π β π΅) β§ π β π΅) β§ π β π΅) β ((π βͺ π) β π β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
57 | 56 | reximdva 3167 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π β π΅) β (βπ β π΅ (π βͺ π) β π β βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
58 | 57 | ralimdva 3166 |
. . . . 5
β’ ((π β§ π β π΅) β (βπ β π΅ βπ β π΅ (π βͺ π) β π β βπ β π΅ βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
59 | 58 | ralimdva 3166 |
. . . 4
β’ (π β (βπ β π΅ βπ β π΅ βπ β π΅ (π βͺ π) β π β βπ β π΅ βπ β π΅ βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
60 | 13, 59 | mpd 15 |
. . 3
β’ (π β βπ β π΅ βπ β π΅ βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
61 | | uneq1 4156 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ) β (π₯ βͺ π¦) = ((πΉβπ) βͺ π¦)) |
62 | 61 | sseq1d 4013 |
. . . . . . . 8
β’ (π₯ = (πΉβπ) β ((π₯ βͺ π¦) β π§ β ((πΉβπ) βͺ π¦) β π§)) |
63 | 62 | rexbidv 3177 |
. . . . . . 7
β’ (π₯ = (πΉβπ) β (βπ§ β (πΉ β π΅)(π₯ βͺ π¦) β π§ β βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§)) |
64 | 63 | ralbidv 3176 |
. . . . . 6
β’ (π₯ = (πΉβπ) β (βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)(π₯ βͺ π¦) β π§ β βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§)) |
65 | 64 | ralima 7242 |
. . . . 5
β’ ((πΉ Fn π« π΄ β§ π΅ β π« π΄) β (βπ₯ β (πΉ β π΅)βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)(π₯ βͺ π¦) β π§ β βπ β π΅ βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§)) |
66 | 7, 8, 65 | syl2anc 583 |
. . . 4
β’ (π β (βπ₯ β (πΉ β π΅)βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)(π₯ βͺ π¦) β π§ β βπ β π΅ βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§)) |
67 | | uneq2 4157 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β ((πΉβπ) βͺ π¦) = ((πΉβπ) βͺ (πΉβπ))) |
68 | 67 | sseq1d 4013 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ) β (((πΉβπ) βͺ π¦) β π§ β ((πΉβπ) βͺ (πΉβπ)) β π§)) |
69 | 68 | rexbidv 3177 |
. . . . . . . 8
β’ (π¦ = (πΉβπ) β (βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§ β βπ§ β (πΉ β π΅)((πΉβπ) βͺ (πΉβπ)) β π§)) |
70 | 69 | ralima 7242 |
. . . . . . 7
β’ ((πΉ Fn π« π΄ β§ π΅ β π« π΄) β (βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§ β βπ β π΅ βπ§ β (πΉ β π΅)((πΉβπ) βͺ (πΉβπ)) β π§)) |
71 | 7, 8, 70 | syl2anc 583 |
. . . . . 6
β’ (π β (βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§ β βπ β π΅ βπ§ β (πΉ β π΅)((πΉβπ) βͺ (πΉβπ)) β π§)) |
72 | | sseq2 4008 |
. . . . . . . . 9
β’ (π§ = (πΉβπ) β (((πΉβπ) βͺ (πΉβπ)) β π§ β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
73 | 72 | rexima 7241 |
. . . . . . . 8
β’ ((πΉ Fn π« π΄ β§ π΅ β π« π΄) β (βπ§ β (πΉ β π΅)((πΉβπ) βͺ (πΉβπ)) β π§ β βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
74 | 7, 8, 73 | syl2anc 583 |
. . . . . . 7
β’ (π β (βπ§ β (πΉ β π΅)((πΉβπ) βͺ (πΉβπ)) β π§ β βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
75 | 74 | ralbidv 3176 |
. . . . . 6
β’ (π β (βπ β π΅ βπ§ β (πΉ β π΅)((πΉβπ) βͺ (πΉβπ)) β π§ β βπ β π΅ βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
76 | 71, 75 | bitrd 279 |
. . . . 5
β’ (π β (βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§ β βπ β π΅ βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
77 | 76 | ralbidv 3176 |
. . . 4
β’ (π β (βπ β π΅ βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)((πΉβπ) βͺ π¦) β π§ β βπ β π΅ βπ β π΅ βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
78 | 66, 77 | bitrd 279 |
. . 3
β’ (π β (βπ₯ β (πΉ β π΅)βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)(π₯ βͺ π¦) β π§ β βπ β π΅ βπ β π΅ βπ β π΅ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
79 | 60, 78 | mpbird 257 |
. 2
β’ (π β βπ₯ β (πΉ β π΅)βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)(π₯ βͺ π¦) β π§) |
80 | | isipodrs 18495 |
. 2
β’
((toIncβ(πΉ
β π΅)) β Dirset
β ((πΉ β π΅) β V β§ (πΉ β π΅) β β
β§ βπ₯ β (πΉ β π΅)βπ¦ β (πΉ β π΅)βπ§ β (πΉ β π΅)(π₯ βͺ π¦) β π§)) |
81 | 2, 12, 79, 80 | syl3anbrc 1342 |
1
β’ (π β (toIncβ(πΉ β π΅)) β Dirset) |