Step | Hyp | Ref
| Expression |
1 | | elfvex 6881 |
. . . . . . 7
β’ (π β (UnifOnβπ) β π β V) |
2 | | isust 23571 |
. . . . . . 7
β’ (π β V β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β (UnifOnβπ) β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) |
4 | 3 | ibi 267 |
. . . . 5
β’ (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)))) |
5 | 4 | adantl 483 |
. . . 4
β’ ((π β β
β§ π β (UnifOnβπ)) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)))) |
6 | 5 | simp1d 1143 |
. . 3
β’ ((π β β
β§ π β (UnifOnβπ)) β π β π« (π Γ π)) |
7 | 5 | simp2d 1144 |
. . . . 5
β’ ((π β β
β§ π β (UnifOnβπ)) β (π Γ π) β π) |
8 | 7 | ne0d 4296 |
. . . 4
β’ ((π β β
β§ π β (UnifOnβπ)) β π β β
) |
9 | 5 | simp3d 1145 |
. . . . . . . . . 10
β’ ((π β β
β§ π β (UnifOnβπ)) β βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) |
10 | 9 | r19.21bi 3233 |
. . . . . . . . 9
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))) |
11 | 10 | simp3d 1145 |
. . . . . . . 8
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£)) |
12 | 11 | simp1d 1143 |
. . . . . . 7
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β ( I βΎ π) β π£) |
13 | | opelidres 5950 |
. . . . . . . . . . . . 13
β’ (π€ β V β (β¨π€, π€β© β ( I βΎ π) β π€ β π)) |
14 | 13 | elv 3450 |
. . . . . . . . . . . 12
β’
(β¨π€, π€β© β ( I βΎ π) β π€ β π) |
15 | 14 | biimpri 227 |
. . . . . . . . . . 11
β’ (π€ β π β β¨π€, π€β© β ( I βΎ π)) |
16 | 15 | rgen 3063 |
. . . . . . . . . 10
β’
βπ€ β
π β¨π€, π€β© β ( I βΎ π) |
17 | | r19.2z 4453 |
. . . . . . . . . 10
β’ ((π β β
β§
βπ€ β π β¨π€, π€β© β ( I βΎ π)) β βπ€ β π β¨π€, π€β© β ( I βΎ π)) |
18 | 16, 17 | mpan2 690 |
. . . . . . . . 9
β’ (π β β
β
βπ€ β π β¨π€, π€β© β ( I βΎ π)) |
19 | 18 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β βπ€ β π β¨π€, π€β© β ( I βΎ π)) |
20 | | ne0i 4295 |
. . . . . . . . 9
β’
(β¨π€, π€β© β ( I βΎ π) β ( I βΎ π) β β
) |
21 | 20 | rexlimivw 3145 |
. . . . . . . 8
β’
(βπ€ β
π β¨π€, π€β© β ( I βΎ π) β ( I βΎ π) β β
) |
22 | 19, 21 | syl 17 |
. . . . . . 7
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β ( I βΎ π) β β
) |
23 | | ssn0 4361 |
. . . . . . 7
β’ ((( I
βΎ π) β π£ β§ ( I βΎ π) β β
) β π£ β β
) |
24 | 12, 22, 23 | syl2anc 585 |
. . . . . 6
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β π£ β β
) |
25 | 24 | nelrdva 3664 |
. . . . 5
β’ ((π β β
β§ π β (UnifOnβπ)) β Β¬ β
β
π) |
26 | | df-nel 3047 |
. . . . 5
β’ (β
β π β Β¬
β
β π) |
27 | 25, 26 | sylibr 233 |
. . . 4
β’ ((π β β
β§ π β (UnifOnβπ)) β β
β π) |
28 | 10 | simp2d 1144 |
. . . . . . . . 9
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β βπ€ β π (π£ β© π€) β π) |
29 | 28 | r19.21bi 3233 |
. . . . . . . 8
β’ ((((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β§ π€ β π) β (π£ β© π€) β π) |
30 | | vex 3448 |
. . . . . . . . . . 11
β’ π€ β V |
31 | 30 | inex2 5276 |
. . . . . . . . . 10
β’ (π£ β© π€) β V |
32 | 31 | pwid 4583 |
. . . . . . . . 9
β’ (π£ β© π€) β π« (π£ β© π€) |
33 | 32 | a1i 11 |
. . . . . . . 8
β’ ((((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β§ π€ β π) β (π£ β© π€) β π« (π£ β© π€)) |
34 | 29, 33 | elind 4155 |
. . . . . . 7
β’ ((((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β§ π€ β π) β (π£ β© π€) β (π β© π« (π£ β© π€))) |
35 | 34 | ne0d 4296 |
. . . . . 6
β’ ((((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β§ π€ β π) β (π β© π« (π£ β© π€)) β β
) |
36 | 35 | ralrimiva 3140 |
. . . . 5
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β βπ€ β π (π β© π« (π£ β© π€)) β β
) |
37 | 36 | ralrimiva 3140 |
. . . 4
β’ ((π β β
β§ π β (UnifOnβπ)) β βπ£ β π βπ€ β π (π β© π« (π£ β© π€)) β β
) |
38 | 8, 27, 37 | 3jca 1129 |
. . 3
β’ ((π β β
β§ π β (UnifOnβπ)) β (π β β
β§ β
β π β§ βπ£ β π βπ€ β π (π β© π« (π£ β© π€)) β β
)) |
39 | 1, 1 | xpexd 7686 |
. . . . 5
β’ (π β (UnifOnβπ) β (π Γ π) β V) |
40 | | isfbas 23196 |
. . . . 5
β’ ((π Γ π) β V β (π β (fBasβ(π Γ π)) β (π β π« (π Γ π) β§ (π β β
β§ β
β π β§ βπ£ β π βπ€ β π (π β© π« (π£ β© π€)) β β
)))) |
41 | 39, 40 | syl 17 |
. . . 4
β’ (π β (UnifOnβπ) β (π β (fBasβ(π Γ π)) β (π β π« (π Γ π) β§ (π β β
β§ β
β π β§ βπ£ β π βπ€ β π (π β© π« (π£ β© π€)) β β
)))) |
42 | 41 | adantl 483 |
. . 3
β’ ((π β β
β§ π β (UnifOnβπ)) β (π β (fBasβ(π Γ π)) β (π β π« (π Γ π) β§ (π β β
β§ β
β π β§ βπ£ β π βπ€ β π (π β© π« (π£ β© π€)) β β
)))) |
43 | 6, 38, 42 | mpbir2and 712 |
. 2
β’ ((π β β
β§ π β (UnifOnβπ)) β π β (fBasβ(π Γ π))) |
44 | | n0 4307 |
. . . . 5
β’ ((π β© π« π€) β β
β
βπ£ π£ β (π β© π« π€)) |
45 | | elin 3927 |
. . . . . . 7
β’ (π£ β (π β© π« π€) β (π£ β π β§ π£ β π« π€)) |
46 | | velpw 4566 |
. . . . . . . 8
β’ (π£ β π« π€ β π£ β π€) |
47 | 46 | anbi2i 624 |
. . . . . . 7
β’ ((π£ β π β§ π£ β π« π€) β (π£ β π β§ π£ β π€)) |
48 | 45, 47 | bitri 275 |
. . . . . 6
β’ (π£ β (π β© π« π€) β (π£ β π β§ π£ β π€)) |
49 | 48 | exbii 1851 |
. . . . 5
β’
(βπ£ π£ β (π β© π« π€) β βπ£(π£ β π β§ π£ β π€)) |
50 | 44, 49 | bitri 275 |
. . . 4
β’ ((π β© π« π€) β β
β
βπ£(π£ β π β§ π£ β π€)) |
51 | 10 | simp1d 1143 |
. . . . . . . 8
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β βπ€ β π« (π Γ π)(π£ β π€ β π€ β π)) |
52 | 51 | r19.21bi 3233 |
. . . . . . 7
β’ ((((π β β
β§ π β (UnifOnβπ)) β§ π£ β π) β§ π€ β π« (π Γ π)) β (π£ β π€ β π€ β π)) |
53 | 52 | an32s 651 |
. . . . . 6
β’ ((((π β β
β§ π β (UnifOnβπ)) β§ π€ β π« (π Γ π)) β§ π£ β π) β (π£ β π€ β π€ β π)) |
54 | 53 | expimpd 455 |
. . . . 5
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π€ β π« (π Γ π)) β ((π£ β π β§ π£ β π€) β π€ β π)) |
55 | 54 | exlimdv 1937 |
. . . 4
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π€ β π« (π Γ π)) β (βπ£(π£ β π β§ π£ β π€) β π€ β π)) |
56 | 50, 55 | biimtrid 241 |
. . 3
β’ (((π β β
β§ π β (UnifOnβπ)) β§ π€ β π« (π Γ π)) β ((π β© π« π€) β β
β π€ β π)) |
57 | 56 | ralrimiva 3140 |
. 2
β’ ((π β β
β§ π β (UnifOnβπ)) β βπ€ β π« (π Γ π)((π β© π« π€) β β
β π€ β π)) |
58 | | isfil 23214 |
. 2
β’ (π β (Filβ(π Γ π)) β (π β (fBasβ(π Γ π)) β§ βπ€ β π« (π Γ π)((π β© π« π€) β β
β π€ β π))) |
59 | 43, 57, 58 | sylanbrc 584 |
1
β’ ((π β β
β§ π β (UnifOnβπ)) β π β (Filβ(π Γ π))) |