Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β π β (UnifOnβπ)) |
2 | 1 | elfvexd 6923 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β π β V) |
3 | | isust 24058 |
. . . . . 6
β’ (π β V β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
5 | 1, 4 | mpbid 231 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)))) |
6 | 5 | simp3d 1141 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) |
7 | | simp1 1133 |
. . . 4
β’
((βπ€ β
π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)) β βπ€ β π« (π Γ π)(π£ β π€ β π€ β π)) |
8 | 7 | ralimi 3077 |
. . 3
β’
(βπ£ β
π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)) β βπ£ β π βπ€ β π« (π Γ π)(π£ β π€ β π€ β π)) |
9 | 6, 8 | syl 17 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β βπ£ β π βπ€ β π« (π Γ π)(π£ β π€ β π€ β π)) |
10 | | simp2 1134 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β π β π) |
11 | 2, 2 | xpexd 7734 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β (π Γ π) β V) |
12 | | simp3 1135 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β π β (π Γ π)) |
13 | 11, 12 | sselpwd 5319 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β π β π« (π Γ π)) |
14 | | sseq1 4002 |
. . . . 5
β’ (π£ = π β (π£ β π€ β π β π€)) |
15 | 14 | imbi1d 341 |
. . . 4
β’ (π£ = π β ((π£ β π€ β π€ β π) β (π β π€ β π€ β π))) |
16 | | sseq2 4003 |
. . . . 5
β’ (π€ = π β (π β π€ β π β π)) |
17 | | eleq1 2815 |
. . . . 5
β’ (π€ = π β (π€ β π β π β π)) |
18 | 16, 17 | imbi12d 344 |
. . . 4
β’ (π€ = π β ((π β π€ β π€ β π) β (π β π β π β π))) |
19 | 15, 18 | rspc2v 3617 |
. . 3
β’ ((π β π β§ π β π« (π Γ π)) β (βπ£ β π βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β (π β π β π β π))) |
20 | 10, 13, 19 | syl2anc 583 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β (βπ£ β π βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β (π β π β π β π))) |
21 | 9, 20 | mpd 15 |
1
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β (π β π β π β π)) |