Step | Hyp | Ref
| Expression |
1 | | mresspw 17536 |
. . . . 5
β’ (π β (Mooreβπ) β π β π« π) |
2 | | velpw 4608 |
. . . . 5
β’ (π β π« π«
π β π β π« π) |
3 | 1, 2 | sylibr 233 |
. . . 4
β’ (π β (Mooreβπ) β π β π« π« π) |
4 | 3 | ssriv 3987 |
. . 3
β’
(Mooreβπ)
β π« π« π |
5 | 4 | a1i 11 |
. 2
β’ (π β π β (Mooreβπ) β π« π« π) |
6 | | ssidd 4006 |
. . 3
β’ (π β π β π« π β π« π) |
7 | | pwidg 4623 |
. . 3
β’ (π β π β π β π« π) |
8 | | intssuni2 4978 |
. . . . . 6
β’ ((π β π« π β§ π β β
) β β© π
β βͺ π« π) |
9 | 8 | 3adant1 1131 |
. . . . 5
β’ ((π β π β§ π β π« π β§ π β β
) β β© π
β βͺ π« π) |
10 | | unipw 5451 |
. . . . 5
β’ βͺ π« π = π |
11 | 9, 10 | sseqtrdi 4033 |
. . . 4
β’ ((π β π β§ π β π« π β§ π β β
) β β© π
β π) |
12 | | elpw2g 5345 |
. . . . 5
β’ (π β π β (β© π β π« π β β© π
β π)) |
13 | 12 | 3ad2ant1 1134 |
. . . 4
β’ ((π β π β§ π β π« π β§ π β β
) β (β© π
β π« π β
β© π β π)) |
14 | 11, 13 | mpbird 257 |
. . 3
β’ ((π β π β§ π β π« π β§ π β β
) β β© π
β π« π) |
15 | 6, 7, 14 | ismred 17546 |
. 2
β’ (π β π β π« π β (Mooreβπ)) |
16 | | n0 4347 |
. . . . 5
β’ (π β β
β
βπ π β π) |
17 | | intss1 4968 |
. . . . . . . . 9
β’ (π β π β β© π β π) |
18 | 17 | adantl 483 |
. . . . . . . 8
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β β© π β π) |
19 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β π β§ π β (Mooreβπ)) β π β (Mooreβπ)) |
20 | 19 | sselda 3983 |
. . . . . . . . 9
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β π β (Mooreβπ)) |
21 | | mresspw 17536 |
. . . . . . . . 9
β’ (π β (Mooreβπ) β π β π« π) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β π β π« π) |
23 | 18, 22 | sstrd 3993 |
. . . . . . 7
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β β© π β π« π) |
24 | 23 | ex 414 |
. . . . . 6
β’ ((π β π β§ π β (Mooreβπ)) β (π β π β β© π β π« π)) |
25 | 24 | exlimdv 1937 |
. . . . 5
β’ ((π β π β§ π β (Mooreβπ)) β (βπ π β π β β© π β π« π)) |
26 | 16, 25 | biimtrid 241 |
. . . 4
β’ ((π β π β§ π β (Mooreβπ)) β (π β β
β β© π
β π« π)) |
27 | 26 | 3impia 1118 |
. . 3
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β β© π
β π« π) |
28 | | simp2 1138 |
. . . . . . 7
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β π β (Mooreβπ)) |
29 | 28 | sselda 3983 |
. . . . . 6
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β π) β π β (Mooreβπ)) |
30 | | mre1cl 17538 |
. . . . . 6
β’ (π β (Mooreβπ) β π β π) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β π) β π β π) |
32 | 31 | ralrimiva 3147 |
. . . 4
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β βπ β π π β π) |
33 | | elintg 4959 |
. . . . 5
β’ (π β π β (π β β© π β βπ β π π β π)) |
34 | 33 | 3ad2ant1 1134 |
. . . 4
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β (π β β© π β βπ β π π β π)) |
35 | 32, 34 | mpbird 257 |
. . 3
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β π β β© π) |
36 | | simp12 1205 |
. . . . . . 7
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β π β (Mooreβπ)) |
37 | 36 | sselda 3983 |
. . . . . 6
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β (Mooreβπ)) |
38 | | simpl2 1193 |
. . . . . . 7
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β β© π) |
39 | | intss1 4968 |
. . . . . . . 8
β’ (π β π β β© π β π) |
40 | 39 | adantl 483 |
. . . . . . 7
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β β© π β π) |
41 | 38, 40 | sstrd 3993 |
. . . . . 6
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β π) |
42 | | simpl3 1194 |
. . . . . 6
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β β
) |
43 | | mreintcl 17539 |
. . . . . 6
β’ ((π β (Mooreβπ) β§ π β π β§ π β β
) β β© π
β π) |
44 | 37, 41, 42, 43 | syl3anc 1372 |
. . . . 5
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β β© π β π) |
45 | 44 | ralrimiva 3147 |
. . . 4
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β βπ β π β© π β π) |
46 | | intex 5338 |
. . . . . 6
β’ (π β β
β β© π
β V) |
47 | | elintg 4959 |
. . . . . 6
β’ (β© π
β V β (β© π β β© π β βπ β π β© π β π)) |
48 | 46, 47 | sylbi 216 |
. . . . 5
β’ (π β β
β (β© π
β β© π β βπ β π β© π β π)) |
49 | 48 | 3ad2ant3 1136 |
. . . 4
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β (β© π
β β© π β βπ β π β© π β π)) |
50 | 45, 49 | mpbird 257 |
. . 3
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β β© π
β β© π) |
51 | 27, 35, 50 | ismred 17546 |
. 2
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β β© π
β (Mooreβπ)) |
52 | 5, 15, 51 | ismred 17546 |
1
β’ (π β π β (Mooreβπ) β (Mooreβπ« π)) |