Step | Hyp | Ref
| Expression |
1 | | ustval 23570 |
. . 3
β’ (π β π β (UnifOnβπ) = {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) |
2 | 1 | eleq2d 2820 |
. 2
β’ (π β π β (π β (UnifOnβπ) β π β {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))})) |
3 | | simp1 1137 |
. . . 4
β’ ((π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) β π β π« (π Γ π)) |
4 | | sqxpexg 7690 |
. . . . . . . 8
β’ (π β π β (π Γ π) β V) |
5 | 4 | pwexd 5335 |
. . . . . . 7
β’ (π β π β π« (π Γ π) β V) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β π β§ π β π« (π Γ π)) β π« (π Γ π) β V) |
7 | | simpr 486 |
. . . . . 6
β’ ((π β π β§ π β π« (π Γ π)) β π β π« (π Γ π)) |
8 | 6, 7 | ssexd 5282 |
. . . . 5
β’ ((π β π β§ π β π« (π Γ π)) β π β V) |
9 | 8 | ex 414 |
. . . 4
β’ (π β π β (π β π« (π Γ π) β π β V)) |
10 | 3, 9 | syl5 34 |
. . 3
β’ (π β π β ((π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) β π β V)) |
11 | | sseq1 3970 |
. . . . 5
β’ (π’ = π β (π’ β π« (π Γ π) β π β π« (π Γ π))) |
12 | | eleq2 2823 |
. . . . 5
β’ (π’ = π β ((π Γ π) β π’ β (π Γ π) β π)) |
13 | | eleq2 2823 |
. . . . . . . . 9
β’ (π’ = π β (π€ β π’ β π€ β π)) |
14 | 13 | imbi2d 341 |
. . . . . . . 8
β’ (π’ = π β ((π£ β π€ β π€ β π’) β (π£ β π€ β π€ β π))) |
15 | 14 | ralbidv 3171 |
. . . . . . 7
β’ (π’ = π β (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β βπ€ β π« (π Γ π)(π£ β π€ β π€ β π))) |
16 | | eleq2 2823 |
. . . . . . . 8
β’ (π’ = π β ((π£ β© π€) β π’ β (π£ β© π€) β π)) |
17 | 16 | raleqbi1dv 3306 |
. . . . . . 7
β’ (π’ = π β (βπ€ β π’ (π£ β© π€) β π’ β βπ€ β π (π£ β© π€) β π)) |
18 | | eleq2 2823 |
. . . . . . . 8
β’ (π’ = π β (β‘π£ β π’ β β‘π£ β π)) |
19 | | rexeq 3309 |
. . . . . . . 8
β’ (π’ = π β (βπ€ β π’ (π€ β π€) β π£ β βπ€ β π (π€ β π€) β π£)) |
20 | 18, 19 | 3anbi23d 1440 |
. . . . . . 7
β’ (π’ = π β ((( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£) β (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) |
21 | 15, 17, 20 | 3anbi123d 1437 |
. . . . . 6
β’ (π’ = π β ((βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)) β (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)))) |
22 | 21 | raleqbi1dv 3306 |
. . . . 5
β’ (π’ = π β (βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)) β βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)))) |
23 | 11, 12, 22 | 3anbi123d 1437 |
. . . 4
β’ (π’ = π β ((π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£))) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
24 | 23 | elab3g 3638 |
. . 3
β’ (((π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) β π β V) β (π β {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
25 | 10, 24 | syl 17 |
. 2
β’ (π β π β (π β {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))} β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
26 | 2, 25 | bitrd 279 |
1
β’ (π β π β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |