Step | Hyp | Ref
| Expression |
1 | | mresspw 17532 |
. . . . 5
β’ (π β (Mooreβπ) β π β π« π) |
2 | | velpw 4606 |
. . . . 5
β’ (π β π« π«
π β π β π« π) |
3 | 1, 2 | sylibr 233 |
. . . 4
β’ (π β (Mooreβπ) β π β π« π« π) |
4 | 3 | ssriv 3985 |
. . 3
β’
(Mooreβπ)
β π« π« π |
5 | 4 | a1i 11 |
. 2
β’ (π β π β (Mooreβπ) β π« π« π) |
6 | | ssidd 4004 |
. . 3
β’ (π β π β π« π β π« π) |
7 | | pwidg 4621 |
. . 3
β’ (π β π β π β π« π) |
8 | | intssuni2 4976 |
. . . . . 6
β’ ((π β π« π β§ π β β
) β β© π
β βͺ π« π) |
9 | 8 | 3adant1 1130 |
. . . . 5
β’ ((π β π β§ π β π« π β§ π β β
) β β© π
β βͺ π« π) |
10 | | unipw 5449 |
. . . . 5
β’ βͺ π« π = π |
11 | 9, 10 | sseqtrdi 4031 |
. . . 4
β’ ((π β π β§ π β π« π β§ π β β
) β β© π
β π) |
12 | | elpw2g 5343 |
. . . . 5
β’ (π β π β (β© π β π« π β β© π
β π)) |
13 | 12 | 3ad2ant1 1133 |
. . . 4
β’ ((π β π β§ π β π« π β§ π β β
) β (β© π
β π« π β
β© π β π)) |
14 | 11, 13 | mpbird 256 |
. . 3
β’ ((π β π β§ π β π« π β§ π β β
) β β© π
β π« π) |
15 | 6, 7, 14 | ismred 17542 |
. 2
β’ (π β π β π« π β (Mooreβπ)) |
16 | | n0 4345 |
. . . . 5
β’ (π β β
β
βπ π β π) |
17 | | intss1 4966 |
. . . . . . . . 9
β’ (π β π β β© π β π) |
18 | 17 | adantl 482 |
. . . . . . . 8
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β β© π β π) |
19 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β π β§ π β (Mooreβπ)) β π β (Mooreβπ)) |
20 | 19 | sselda 3981 |
. . . . . . . . 9
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β π β (Mooreβπ)) |
21 | | mresspw 17532 |
. . . . . . . . 9
β’ (π β (Mooreβπ) β π β π« π) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β π β π« π) |
23 | 18, 22 | sstrd 3991 |
. . . . . . 7
β’ (((π β π β§ π β (Mooreβπ)) β§ π β π) β β© π β π« π) |
24 | 23 | ex 413 |
. . . . . 6
β’ ((π β π β§ π β (Mooreβπ)) β (π β π β β© π β π« π)) |
25 | 24 | exlimdv 1936 |
. . . . 5
β’ ((π β π β§ π β (Mooreβπ)) β (βπ π β π β β© π β π« π)) |
26 | 16, 25 | biimtrid 241 |
. . . 4
β’ ((π β π β§ π β (Mooreβπ)) β (π β β
β β© π
β π« π)) |
27 | 26 | 3impia 1117 |
. . 3
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β β© π
β π« π) |
28 | | simp2 1137 |
. . . . . . 7
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β π β (Mooreβπ)) |
29 | 28 | sselda 3981 |
. . . . . 6
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β π) β π β (Mooreβπ)) |
30 | | mre1cl 17534 |
. . . . . 6
β’ (π β (Mooreβπ) β π β π) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β π) β π β π) |
32 | 31 | ralrimiva 3146 |
. . . 4
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β βπ β π π β π) |
33 | | elintg 4957 |
. . . . 5
β’ (π β π β (π β β© π β βπ β π π β π)) |
34 | 33 | 3ad2ant1 1133 |
. . . 4
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β (π β β© π β βπ β π π β π)) |
35 | 32, 34 | mpbird 256 |
. . 3
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β π β β© π) |
36 | | simp12 1204 |
. . . . . . 7
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β π β (Mooreβπ)) |
37 | 36 | sselda 3981 |
. . . . . 6
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β (Mooreβπ)) |
38 | | simpl2 1192 |
. . . . . . 7
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β β© π) |
39 | | intss1 4966 |
. . . . . . . 8
β’ (π β π β β© π β π) |
40 | 39 | adantl 482 |
. . . . . . 7
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β β© π β π) |
41 | 38, 40 | sstrd 3991 |
. . . . . 6
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β π) |
42 | | simpl3 1193 |
. . . . . 6
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β π β β
) |
43 | | mreintcl 17535 |
. . . . . 6
β’ ((π β (Mooreβπ) β§ π β π β§ π β β
) β β© π
β π) |
44 | 37, 41, 42, 43 | syl3anc 1371 |
. . . . 5
β’ ((((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β§ π β π) β β© π β π) |
45 | 44 | ralrimiva 3146 |
. . . 4
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β βπ β π β© π β π) |
46 | | intex 5336 |
. . . . . 6
β’ (π β β
β β© π
β V) |
47 | | elintg 4957 |
. . . . . 6
β’ (β© π
β V β (β© π β β© π β βπ β π β© π β π)) |
48 | 46, 47 | sylbi 216 |
. . . . 5
β’ (π β β
β (β© π
β β© π β βπ β π β© π β π)) |
49 | 48 | 3ad2ant3 1135 |
. . . 4
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β (β© π
β β© π β βπ β π β© π β π)) |
50 | 45, 49 | mpbird 256 |
. . 3
β’ (((π β π β§ π β (Mooreβπ) β§ π β β
) β§ π β β© π β§ π β β
) β β© π
β β© π) |
51 | 27, 35, 50 | ismred 17542 |
. 2
β’ ((π β π β§ π β (Mooreβπ) β§ π β β
) β β© π
β (Mooreβπ)) |
52 | 5, 15, 51 | ismred 17542 |
1
β’ (π β π β (Mooreβπ) β (Mooreβπ« π)) |