Step | Hyp | Ref
| Expression |
1 | | df-ust 23568 |
. 2
β’ UnifOn =
(π₯ β V β¦ {π’ β£ (π’ β π« (π₯ Γ π₯) β§ (π₯ Γ π₯) β π’ β§ βπ£ β π’ (βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) |
2 | | id 22 |
. . . . . . 7
β’ (π₯ = π β π₯ = π) |
3 | 2 | sqxpeqd 5666 |
. . . . . 6
β’ (π₯ = π β (π₯ Γ π₯) = (π Γ π)) |
4 | 3 | pweqd 4578 |
. . . . 5
β’ (π₯ = π β π« (π₯ Γ π₯) = π« (π Γ π)) |
5 | 4 | sseq2d 3977 |
. . . 4
β’ (π₯ = π β (π’ β π« (π₯ Γ π₯) β π’ β π« (π Γ π))) |
6 | 3 | eleq1d 2819 |
. . . 4
β’ (π₯ = π β ((π₯ Γ π₯) β π’ β (π Γ π) β π’)) |
7 | 4 | raleqdv 3312 |
. . . . . 6
β’ (π₯ = π β (βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’))) |
8 | | reseq2 5933 |
. . . . . . . 8
β’ (π₯ = π β ( I βΎ π₯) = ( I βΎ π)) |
9 | 8 | sseq1d 3976 |
. . . . . . 7
β’ (π₯ = π β (( I βΎ π₯) β π£ β ( I βΎ π) β π£)) |
10 | 9 | 3anbi1d 1441 |
. . . . . 6
β’ (π₯ = π β ((( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£) β (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£))) |
11 | 7, 10 | 3anbi13d 1439 |
. . . . 5
β’ (π₯ = π β ((βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)) β (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))) |
12 | 11 | ralbidv 3171 |
. . . 4
β’ (π₯ = π β (βπ£ β π’ (βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)) β βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))) |
13 | 5, 6, 12 | 3anbi123d 1437 |
. . 3
β’ (π₯ = π β ((π’ β π« (π₯ Γ π₯) β§ (π₯ Γ π₯) β π’ β§ βπ£ β π’ (βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£))) β (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£))))) |
14 | 13 | abbidv 2802 |
. 2
β’ (π₯ = π β {π’ β£ (π’ β π« (π₯ Γ π₯) β§ (π₯ Γ π₯) β π’ β§ βπ£ β π’ (βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} = {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) |
15 | | elex 3462 |
. 2
β’ (π β π β π β V) |
16 | | simp1 1137 |
. . . . 5
β’ ((π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£))) β π’ β π« (π Γ π)) |
17 | 16 | ss2abi 4024 |
. . . 4
β’ {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} β {π’ β£ π’ β π« (π Γ π)} |
18 | | df-pw 4563 |
. . . 4
β’ π«
π« (π Γ π) = {π’ β£ π’ β π« (π Γ π)} |
19 | 17, 18 | sseqtrri 3982 |
. . 3
β’ {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} β π« π« (π Γ π) |
20 | | sqxpexg 7690 |
. . . 4
β’ (π β π β (π Γ π) β V) |
21 | | pwexg 5334 |
. . . 4
β’ ((π Γ π) β V β π« (π Γ π) β V) |
22 | | pwexg 5334 |
. . . 4
β’
(π« (π
Γ π) β V β
π« π« (π
Γ π) β
V) |
23 | 20, 21, 22 | 3syl 18 |
. . 3
β’ (π β π β π« π« (π Γ π) β V) |
24 | | ssexg 5281 |
. . 3
β’ (({π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} β π« π« (π Γ π) β§ π« π« (π Γ π) β V) β {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} β V) |
25 | 19, 23, 24 | sylancr 588 |
. 2
β’ (π β π β {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} β V) |
26 | 1, 14, 15, 25 | fvmptd3 6972 |
1
β’ (π β π β (UnifOnβπ) = {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) |