Step | Hyp | Ref
| Expression |
1 | | elfvex 6885 |
. . . . . . . 8
β’ (π β (UnifOnβπ) β π β V) |
2 | | isust 23571 |
. . . . . . . 8
β’ (π β V β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π β (UnifOnβπ) β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
4 | 3 | ibi 267 |
. . . . . 6
β’ (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)))) |
5 | 4 | simp3d 1145 |
. . . . 5
β’ (π β (UnifOnβπ) β βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) |
6 | | sseq1 3974 |
. . . . . . . . 9
β’ (π£ = π β (π£ β π€ β π β π€)) |
7 | 6 | imbi1d 342 |
. . . . . . . 8
β’ (π£ = π β ((π£ β π€ β π€ β π) β (π β π€ β π€ β π))) |
8 | 7 | ralbidv 3175 |
. . . . . . 7
β’ (π£ = π β (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β βπ€ β π« (π Γ π)(π β π€ β π€ β π))) |
9 | | ineq1 4170 |
. . . . . . . . 9
β’ (π£ = π β (π£ β© π€) = (π β© π€)) |
10 | 9 | eleq1d 2823 |
. . . . . . . 8
β’ (π£ = π β ((π£ β© π€) β π β (π β© π€) β π)) |
11 | 10 | ralbidv 3175 |
. . . . . . 7
β’ (π£ = π β (βπ€ β π (π£ β© π€) β π β βπ€ β π (π β© π€) β π)) |
12 | | sseq2 3975 |
. . . . . . . 8
β’ (π£ = π β (( I βΎ π) β π£ β ( I βΎ π) β π)) |
13 | | cnveq 5834 |
. . . . . . . . 9
β’ (π£ = π β β‘π£ = β‘π) |
14 | 13 | eleq1d 2823 |
. . . . . . . 8
β’ (π£ = π β (β‘π£ β π β β‘π β π)) |
15 | | sseq2 3975 |
. . . . . . . . 9
β’ (π£ = π β ((π€ β π€) β π£ β (π€ β π€) β π)) |
16 | 15 | rexbidv 3176 |
. . . . . . . 8
β’ (π£ = π β (βπ€ β π (π€ β π€) β π£ β βπ€ β π (π€ β π€) β π)) |
17 | 12, 14, 16 | 3anbi123d 1437 |
. . . . . . 7
β’ (π£ = π β ((( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£) β (( I βΎ π) β π β§ β‘π β π β§ βπ€ β π (π€ β π€) β π))) |
18 | 8, 11, 17 | 3anbi123d 1437 |
. . . . . 6
β’ (π£ = π β ((βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)) β (βπ€ β π« (π Γ π)(π β π€ β π€ β π) β§ βπ€ β π (π β© π€) β π β§ (( I βΎ π) β π β§ β‘π β π β§ βπ€ β π (π€ β π€) β π)))) |
19 | 18 | rspcv 3580 |
. . . . 5
β’ (π β π β (βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)) β (βπ€ β π« (π Γ π)(π β π€ β π€ β π) β§ βπ€ β π (π β© π€) β π β§ (( I βΎ π) β π β§ β‘π β π β§ βπ€ β π (π€ β π€) β π)))) |
20 | 5, 19 | mpan9 508 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β (βπ€ β π« (π Γ π)(π β π€ β π€ β π) β§ βπ€ β π (π β© π€) β π β§ (( I βΎ π) β π β§ β‘π β π β§ βπ€ β π (π€ β π€) β π))) |
21 | 20 | simp2d 1144 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (π β© π€) β π) |
22 | | ineq2 4171 |
. . . . 5
β’ (π€ = π β (π β© π€) = (π β© π)) |
23 | 22 | eleq1d 2823 |
. . . 4
β’ (π€ = π β ((π β© π€) β π β (π β© π) β π)) |
24 | 23 | rspcv 3580 |
. . 3
β’ (π β π β (βπ€ β π (π β© π€) β π β (π β© π) β π)) |
25 | 21, 24 | mpan9 508 |
. 2
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β π) β (π β© π) β π) |
26 | 25 | 3impa 1111 |
1
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β© π) β π) |