Step | Hyp | Ref
| Expression |
1 | | 0ex 5308 |
. . . . . . . 8
β’ β
β V |
2 | | isust 23708 |
. . . . . . . 8
β’ (β
β V β (π’ β
(UnifOnββ
) β (π’ β π« (β
Γ β
)
β§ (β
Γ β
) β π’ β§ βπ£ β π’ (βπ€ β π« (β
Γ
β
)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ β
) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£))))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
β’ (π’ β (UnifOnββ
)
β (π’ β π«
(β
Γ β
) β§ (β
Γ β
) β π’ β§ βπ£ β π’ (βπ€ β π« (β
Γ
β
)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ β
) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))) |
4 | 3 | simp1bi 1146 |
. . . . . 6
β’ (π’ β (UnifOnββ
)
β π’ β π«
(β
Γ β
)) |
5 | | 0xp 5775 |
. . . . . . . 8
β’ (β
Γ β
) = β
|
6 | 5 | pweqi 4619 |
. . . . . . 7
β’ π«
(β
Γ β
) = π« β
|
7 | | pw0 4816 |
. . . . . . 7
β’ π«
β
= {β
} |
8 | 6, 7 | eqtri 2761 |
. . . . . 6
β’ π«
(β
Γ β
) = {β
} |
9 | 4, 8 | sseqtrdi 4033 |
. . . . 5
β’ (π’ β (UnifOnββ
)
β π’ β
{β
}) |
10 | | ustbasel 23711 |
. . . . . . 7
β’ (π’ β (UnifOnββ
)
β (β
Γ β
) β π’) |
11 | 5, 10 | eqeltrrid 2839 |
. . . . . 6
β’ (π’ β (UnifOnββ
)
β β
β π’) |
12 | 11 | snssd 4813 |
. . . . 5
β’ (π’ β (UnifOnββ
)
β {β
} β π’) |
13 | 9, 12 | eqssd 4000 |
. . . 4
β’ (π’ β (UnifOnββ
)
β π’ =
{β
}) |
14 | | velsn 4645 |
. . . 4
β’ (π’ β {{β
}} β π’ = {β
}) |
15 | 13, 14 | sylibr 233 |
. . 3
β’ (π’ β (UnifOnββ
)
β π’ β
{{β
}}) |
16 | 15 | ssriv 3987 |
. 2
β’
(UnifOnββ
) β {{β
}} |
17 | 8 | eqimss2i 4044 |
. . . 4
β’ {β
}
β π« (β
Γ β
) |
18 | 1 | snid 4665 |
. . . . 5
β’ β
β {β
} |
19 | 5, 18 | eqeltri 2830 |
. . . 4
β’ (β
Γ β
) β {β
} |
20 | 18 | a1i 11 |
. . . . . 6
β’ (β
β β
β β
β {β
}) |
21 | 8 | raleqi 3324 |
. . . . . . 7
β’
(βπ€ β
π« (β
Γ β
)(β
β π€ β π€ β {β
}) β βπ€ β {β
} (β
β π€ β π€ β
{β
})) |
22 | | sseq2 4009 |
. . . . . . . . 9
β’ (π€ = β
β (β
β π€ β β
β β
)) |
23 | | eleq1 2822 |
. . . . . . . . 9
β’ (π€ = β
β (π€ β {β
} β β
β {β
})) |
24 | 22, 23 | imbi12d 345 |
. . . . . . . 8
β’ (π€ = β
β ((β
β π€ β π€ β {β
}) β
(β
β β
β β
β {β
}))) |
25 | 1, 24 | ralsn 4686 |
. . . . . . 7
β’
(βπ€ β
{β
} (β
β π€ β π€ β {β
}) β (β
β
β
β β
β {β
})) |
26 | 21, 25 | bitri 275 |
. . . . . 6
β’
(βπ€ β
π« (β
Γ β
)(β
β π€ β π€ β {β
}) β (β
β
β
β β
β {β
})) |
27 | 20, 26 | mpbir 230 |
. . . . 5
β’
βπ€ β
π« (β
Γ β
)(β
β π€ β π€ β {β
}) |
28 | | inidm 4219 |
. . . . . . 7
β’ (β
β© β
) = β
|
29 | 28, 18 | eqeltri 2830 |
. . . . . 6
β’ (β
β© β
) β {β
} |
30 | | ineq2 4207 |
. . . . . . . 8
β’ (π€ = β
β (β
β©
π€) = (β
β©
β
)) |
31 | 30 | eleq1d 2819 |
. . . . . . 7
β’ (π€ = β
β ((β
β© π€) β {β
}
β (β
β© β
) β {β
})) |
32 | 1, 31 | ralsn 4686 |
. . . . . 6
β’
(βπ€ β
{β
} (β
β© π€)
β {β
} β (β
β© β
) β
{β
}) |
33 | 29, 32 | mpbir 230 |
. . . . 5
β’
βπ€ β
{β
} (β
β© π€)
β {β
} |
34 | | res0 5986 |
. . . . . . 7
β’ ( I
βΎ β
) = β
|
35 | 34 | eqimssi 4043 |
. . . . . 6
β’ ( I
βΎ β
) β β
|
36 | | cnv0 6141 |
. . . . . . 7
β’ β‘β
= β
|
37 | 36, 18 | eqeltri 2830 |
. . . . . 6
β’ β‘β
β {β
} |
38 | | 0trrel 14928 |
. . . . . . 7
β’ (β
β β
) β β
|
39 | | id 22 |
. . . . . . . . . 10
β’ (π€ = β
β π€ = β
) |
40 | 39, 39 | coeq12d 5865 |
. . . . . . . . 9
β’ (π€ = β
β (π€ β π€) = (β
β
β
)) |
41 | 40 | sseq1d 4014 |
. . . . . . . 8
β’ (π€ = β
β ((π€ β π€) β β
β (β
β
β
) β β
)) |
42 | 1, 41 | rexsn 4687 |
. . . . . . 7
β’
(βπ€ β
{β
} (π€ β π€) β β
β
(β
β β
) β β
) |
43 | 38, 42 | mpbir 230 |
. . . . . 6
β’
βπ€ β
{β
} (π€ β π€) β
β
|
44 | 35, 37, 43 | 3pm3.2i 1340 |
. . . . 5
β’ (( I
βΎ β
) β β
β§ β‘β
β {β
} β§ βπ€ β {β
} (π€ β π€) β β
) |
45 | | sseq1 4008 |
. . . . . . . . 9
β’ (π£ = β
β (π£ β π€ β β
β π€)) |
46 | 45 | imbi1d 342 |
. . . . . . . 8
β’ (π£ = β
β ((π£ β π€ β π€ β {β
}) β (β
β
π€ β π€ β {β
}))) |
47 | 46 | ralbidv 3178 |
. . . . . . 7
β’ (π£ = β
β (βπ€ β π« (β
Γ β
)(π£ β
π€ β π€ β {β
}) β βπ€ β π« (β
Γ β
)(β
β π€ β π€ β {β
}))) |
48 | | ineq1 4206 |
. . . . . . . . 9
β’ (π£ = β
β (π£ β© π€) = (β
β© π€)) |
49 | 48 | eleq1d 2819 |
. . . . . . . 8
β’ (π£ = β
β ((π£ β© π€) β {β
} β (β
β©
π€) β
{β
})) |
50 | 49 | ralbidv 3178 |
. . . . . . 7
β’ (π£ = β
β (βπ€ β {β
} (π£ β© π€) β {β
} β βπ€ β {β
} (β
β©
π€) β
{β
})) |
51 | | sseq2 4009 |
. . . . . . . 8
β’ (π£ = β
β (( I βΎ
β
) β π£ β (
I βΎ β
) β β
)) |
52 | | cnveq 5874 |
. . . . . . . . 9
β’ (π£ = β
β β‘π£ = β‘β
) |
53 | 52 | eleq1d 2819 |
. . . . . . . 8
β’ (π£ = β
β (β‘π£ β {β
} β β‘β
β {β
})) |
54 | | sseq2 4009 |
. . . . . . . . 9
β’ (π£ = β
β ((π€ β π€) β π£ β (π€ β π€) β β
)) |
55 | 54 | rexbidv 3179 |
. . . . . . . 8
β’ (π£ = β
β (βπ€ β {β
} (π€ β π€) β π£ β βπ€ β {β
} (π€ β π€) β β
)) |
56 | 51, 53, 55 | 3anbi123d 1437 |
. . . . . . 7
β’ (π£ = β
β ((( I βΎ
β
) β π£ β§
β‘π£ β {β
} β§ βπ€ β {β
} (π€ β π€) β π£) β (( I βΎ β
) β
β
β§ β‘β
β {β
}
β§ βπ€ β
{β
} (π€ β π€) β
β
))) |
57 | 47, 50, 56 | 3anbi123d 1437 |
. . . . . 6
β’ (π£ = β
β
((βπ€ β
π« (β
Γ β
)(π£ β π€ β π€ β {β
}) β§ βπ€ β {β
} (π£ β© π€) β {β
} β§ (( I βΎ
β
) β π£ β§
β‘π£ β {β
} β§ βπ€ β {β
} (π€ β π€) β π£)) β (βπ€ β π« (β
Γ
β
)(β
β π€
β π€ β {β
})
β§ βπ€ β
{β
} (β
β© π€)
β {β
} β§ (( I βΎ β
) β β
β§ β‘β
β {β
} β§ βπ€ β {β
} (π€ β π€) β β
)))) |
58 | 1, 57 | ralsn 4686 |
. . . . 5
β’
(βπ£ β
{β
} (βπ€ β
π« (β
Γ β
)(π£ β π€ β π€ β {β
}) β§ βπ€ β {β
} (π£ β© π€) β {β
} β§ (( I βΎ
β
) β π£ β§
β‘π£ β {β
} β§ βπ€ β {β
} (π€ β π€) β π£)) β (βπ€ β π« (β
Γ
β
)(β
β π€
β π€ β {β
})
β§ βπ€ β
{β
} (β
β© π€)
β {β
} β§ (( I βΎ β
) β β
β§ β‘β
β {β
} β§ βπ€ β {β
} (π€ β π€) β β
))) |
59 | 27, 33, 44, 58 | mpbir3an 1342 |
. . . 4
β’
βπ£ β
{β
} (βπ€ β
π« (β
Γ β
)(π£ β π€ β π€ β {β
}) β§ βπ€ β {β
} (π£ β© π€) β {β
} β§ (( I βΎ
β
) β π£ β§
β‘π£ β {β
} β§ βπ€ β {β
} (π€ β π€) β π£)) |
60 | | isust 23708 |
. . . . 5
β’ (β
β V β ({β
} β (UnifOnββ
) β ({β
}
β π« (β
Γ β
) β§ (β
Γ β
)
β {β
} β§ βπ£ β {β
} (βπ€ β π« (β
Γ
β
)(π£ β π€ β π€ β {β
}) β§ βπ€ β {β
} (π£ β© π€) β {β
} β§ (( I βΎ
β
) β π£ β§
β‘π£ β {β
} β§ βπ€ β {β
} (π€ β π€) β π£))))) |
61 | 1, 60 | ax-mp 5 |
. . . 4
β’
({β
} β (UnifOnββ
) β ({β
} β
π« (β
Γ β
) β§ (β
Γ β
) β
{β
} β§ βπ£
β {β
} (βπ€
β π« (β
Γ β
)(π£ β π€ β π€ β {β
}) β§ βπ€ β {β
} (π£ β© π€) β {β
} β§ (( I βΎ
β
) β π£ β§
β‘π£ β {β
} β§ βπ€ β {β
} (π€ β π€) β π£)))) |
62 | 17, 19, 59, 61 | mpbir3an 1342 |
. . 3
β’ {β
}
β (UnifOnββ
) |
63 | | snssi 4812 |
. . 3
β’
({β
} β (UnifOnββ
) β {{β
}} β
(UnifOnββ
)) |
64 | 62, 63 | ax-mp 5 |
. 2
β’
{{β
}} β (UnifOnββ
) |
65 | 16, 64 | eqssi 3999 |
1
β’
(UnifOnββ
) = {{β
}} |