Step | Hyp | Ref
| Expression |
1 | | simpl1l 1221 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ (π β (πβπ) β§ π€ β π β§ π = (π€ β {π}))) β π β (UnifOnβπ)) |
2 | 1 | 3anassrs 1357 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π β (UnifOnβπ)) |
3 | | simplr 766 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π€ β π) |
4 | | ustssxp 24030 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π€ β π) β π€ β (π Γ π)) |
5 | 2, 3, 4 | syl2anc 583 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π€ β (π Γ π)) |
6 | | simpl1r 1222 |
. . . . . . . . 9
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ (π β (πβπ) β§ π€ β π β§ π = (π€ β {π}))) β π β π) |
7 | 6 | 3anassrs 1357 |
. . . . . . . 8
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π β π) |
8 | 7 | snssd 4804 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β {π} β π) |
9 | | simpl3 1190 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ (π β (πβπ) β§ π€ β π β§ π = (π€ β {π}))) β π β π) |
10 | 9 | 3anassrs 1357 |
. . . . . . 7
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π β π) |
11 | | xpss12 5681 |
. . . . . . 7
β’ (({π} β π β§ π β π) β ({π} Γ π) β (π Γ π)) |
12 | 8, 10, 11 | syl2anc 583 |
. . . . . 6
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β ({π} Γ π) β (π Γ π)) |
13 | 5, 12 | unssd 4178 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β (π€ βͺ ({π} Γ π)) β (π Γ π)) |
14 | | ssun1 4164 |
. . . . . 6
β’ π€ β (π€ βͺ ({π} Γ π)) |
15 | 14 | a1i 11 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π€ β (π€ βͺ ({π} Γ π))) |
16 | | ustssel 24031 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π€ β π β§ (π€ βͺ ({π} Γ π)) β (π Γ π)) β (π€ β (π€ βͺ ({π} Γ π)) β (π€ βͺ ({π} Γ π)) β π)) |
17 | 16 | imp 406 |
. . . . 5
β’ (((π β (UnifOnβπ) β§ π€ β π β§ (π€ βͺ ({π} Γ π)) β (π Γ π)) β§ π€ β (π€ βͺ ({π} Γ π))) β (π€ βͺ ({π} Γ π)) β π) |
18 | 2, 3, 13, 15, 17 | syl31anc 1370 |
. . . 4
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β (π€ βͺ ({π} Γ π)) β π) |
19 | | simpl2 1189 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ (π β (πβπ) β§ π€ β π β§ π = (π€ β {π}))) β π β π) |
20 | 19 | 3anassrs 1357 |
. . . . 5
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π β π) |
21 | | ssequn1 4172 |
. . . . . . 7
β’ (π β π β (π βͺ π) = π) |
22 | 21 | biimpi 215 |
. . . . . 6
β’ (π β π β (π βͺ π) = π) |
23 | | id 22 |
. . . . . . . 8
β’ (π = (π€ β {π}) β π = (π€ β {π})) |
24 | | inidm 4210 |
. . . . . . . . . . 11
β’ ({π} β© {π}) = {π} |
25 | | vex 3470 |
. . . . . . . . . . . 12
β’ π β V |
26 | 25 | snnz 4772 |
. . . . . . . . . . 11
β’ {π} β β
|
27 | 24, 26 | eqnetri 3003 |
. . . . . . . . . 10
β’ ({π} β© {π}) β β
|
28 | | xpima2 6173 |
. . . . . . . . . 10
β’ (({π} β© {π}) β β
β (({π} Γ π) β {π}) = π) |
29 | 27, 28 | mp1i 13 |
. . . . . . . . 9
β’ (π = (π€ β {π}) β (({π} Γ π) β {π}) = π) |
30 | 29 | eqcomd 2730 |
. . . . . . . 8
β’ (π = (π€ β {π}) β π = (({π} Γ π) β {π})) |
31 | 23, 30 | uneq12d 4156 |
. . . . . . 7
β’ (π = (π€ β {π}) β (π βͺ π) = ((π€ β {π}) βͺ (({π} Γ π) β {π}))) |
32 | | imaundir 6140 |
. . . . . . 7
β’ ((π€ βͺ ({π} Γ π)) β {π}) = ((π€ β {π}) βͺ (({π} Γ π) β {π})) |
33 | 31, 32 | eqtr4di 2782 |
. . . . . 6
β’ (π = (π€ β {π}) β (π βͺ π) = ((π€ βͺ ({π} Γ π)) β {π})) |
34 | 22, 33 | sylan9req 2785 |
. . . . 5
β’ ((π β π β§ π = (π€ β {π})) β π = ((π€ βͺ ({π} Γ π)) β {π})) |
35 | 20, 34 | sylancom 587 |
. . . 4
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π = ((π€ βͺ ({π} Γ π)) β {π})) |
36 | | imaeq1 6044 |
. . . . 5
β’ (π’ = (π€ βͺ ({π} Γ π)) β (π’ β {π}) = ((π€ βͺ ({π} Γ π)) β {π})) |
37 | 36 | rspceeqv 3625 |
. . . 4
β’ (((π€ βͺ ({π} Γ π)) β π β§ π = ((π€ βͺ ({π} Γ π)) β {π})) β βπ’ β π π = (π’ β {π})) |
38 | 18, 35, 37 | syl2anc 583 |
. . 3
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β βπ’ β π π = (π’ β {π})) |
39 | | utopustuq.1 |
. . . . . . 7
β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
40 | 39 | ustuqtoplem 24065 |
. . . . . 6
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β V) β (π β (πβπ) β βπ€ β π π = (π€ β {π}))) |
41 | 40 | elvd 3473 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (πβπ) β βπ€ β π π = (π€ β {π}))) |
42 | 41 | biimpa 476 |
. . . 4
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ€ β π π = (π€ β {π})) |
43 | 42 | 3ad2antl1 1182 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β βπ€ β π π = (π€ β {π})) |
44 | 38, 43 | r19.29a 3154 |
. 2
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β βπ’ β π π = (π’ β {π})) |
45 | 39 | ustuqtoplem 24065 |
. . . . 5
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β V) β (π β (πβπ) β βπ’ β π π = (π’ β {π}))) |
46 | 45 | elvd 3473 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (πβπ) β βπ’ β π π = (π’ β {π}))) |
47 | 46 | 3ad2ant1 1130 |
. . 3
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β (π β (πβπ) β βπ’ β π π = (π’ β {π}))) |
48 | 47 | adantr 480 |
. 2
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β (π β (πβπ) β βπ’ β π π = (π’ β {π}))) |
49 | 44, 48 | mpbird 257 |
1
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) |