Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
β’ (Ο
Γ {π}) = (Ο
Γ {π}) |
2 | | omex 9586 |
. . . . . . . 8
β’ Ο
β V |
3 | | snex 5393 |
. . . . . . . 8
β’ {π} β V |
4 | 2, 3 | xpex 7692 |
. . . . . . 7
β’ (Ο
Γ {π}) β
V |
5 | | eqeq1 2741 |
. . . . . . 7
β’ (π = (Ο Γ {π}) β (π = (Ο Γ {π}) β (Ο Γ {π}) = (Ο Γ {π}))) |
6 | 4, 5 | spcev 3568 |
. . . . . 6
β’ ((Ο
Γ {π}) = (Ο
Γ {π}) β
βπ π = (Ο Γ {π})) |
7 | 1, 6 | mp1i 13 |
. . . . 5
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β βπ π = (Ο Γ {π})) |
8 | 3, 2 | pm3.2i 472 |
. . . . . . . 8
β’ ({π} β V β§ Ο β
V) |
9 | | elmapg 8785 |
. . . . . . . 8
β’ (({π} β V β§ Ο β
V) β (π β ({π} βm Ο)
β π:ΟβΆ{π})) |
10 | 8, 9 | mp1i 13 |
. . . . . . 7
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β (π β ({π} βm Ο) β π:ΟβΆ{π})) |
11 | | fconst2g 7157 |
. . . . . . . 8
β’ (π β π β (π:ΟβΆ{π} β π = (Ο Γ {π}))) |
12 | 11 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β (π:ΟβΆ{π} β π = (Ο Γ {π}))) |
13 | 10, 12 | bitrd 279 |
. . . . . 6
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β (π β ({π} βm Ο) β π = (Ο Γ {π}))) |
14 | 13 | exbidv 1925 |
. . . . 5
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β (βπ π β ({π} βm Ο) β
βπ π = (Ο Γ {π}))) |
15 | 7, 14 | mpbird 257 |
. . . 4
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β βπ π β ({π} βm
Ο)) |
16 | | neq0 4310 |
. . . 4
β’ (Β¬
({π} βm
Ο) = β
β βπ π β ({π} βm
Ο)) |
17 | 15, 16 | sylibr 233 |
. . 3
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β Β¬ ({π} βm Ο) =
β
) |
18 | | eqcom 2744 |
. . 3
β’ (({π} βm Ο) =
β
β β
= ({π} βm
Ο)) |
19 | 17, 18 | sylnib 328 |
. 2
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β Β¬ β
= ({π} βm
Ο)) |
20 | | ovex 7395 |
. . . . 5
β’ (πΌβππ½) β V |
21 | 3, 20 | pm3.2i 472 |
. . . 4
β’ ({π} β V β§ (πΌβππ½) β V) |
22 | | prv 34062 |
. . . 4
β’ (({π} β V β§ (πΌβππ½) β V) β ({π}β§(πΌβππ½) β ({π} Satβ (πΌβππ½)) = ({π} βm
Ο))) |
23 | 21, 22 | mp1i 13 |
. . 3
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β ({π}β§(πΌβππ½) β ({π} Satβ (πΌβππ½)) = ({π} βm
Ο))) |
24 | | goel 33981 |
. . . . . . . . 9
β’ ((πΌ β Ο β§ π½ β Ο) β (πΌβππ½) = β¨β
, β¨πΌ, π½β©β©) |
25 | | 0ex 5269 |
. . . . . . . . . . . 12
β’ β
β V |
26 | 25 | snid 4627 |
. . . . . . . . . . 11
β’ β
β {β
} |
27 | 26 | a1i 11 |
. . . . . . . . . 10
β’ ((πΌ β Ο β§ π½ β Ο) β β
β {β
}) |
28 | | opelxpi 5675 |
. . . . . . . . . 10
β’ ((πΌ β Ο β§ π½ β Ο) β
β¨πΌ, π½β© β (Ο Γ
Ο)) |
29 | 27, 28 | opelxpd 5676 |
. . . . . . . . 9
β’ ((πΌ β Ο β§ π½ β Ο) β
β¨β
, β¨πΌ,
π½β©β© β
({β
} Γ (Ο Γ Ο))) |
30 | 24, 29 | eqeltrd 2838 |
. . . . . . . 8
β’ ((πΌ β Ο β§ π½ β Ο) β (πΌβππ½) β ({β
} Γ
(Ο Γ Ο))) |
31 | | fmla0xp 34017 |
. . . . . . . 8
β’
(Fmlaββ
) = ({β
} Γ (Ο Γ
Ο)) |
32 | 30, 31 | eleqtrrdi 2849 |
. . . . . . 7
β’ ((πΌ β Ο β§ π½ β Ο) β (πΌβππ½) β
(Fmlaββ
)) |
33 | 32 | 3adant3 1133 |
. . . . . 6
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β (πΌβππ½) β
(Fmlaββ
)) |
34 | | satefvfmla0 34052 |
. . . . . 6
β’ (({π} β V β§ (πΌβππ½) β (Fmlaββ
))
β ({π}
Satβ (πΌβππ½)) = {π β ({π} βm Ο) β£ (πβ(1st
β(2nd β(πΌβππ½)))) β (πβ(2nd β(2nd
β(πΌβππ½))))}) |
35 | 3, 33, 34 | sylancr 588 |
. . . . 5
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β ({π} Satβ (πΌβππ½)) = {π β ({π} βm Ο) β£ (πβ(1st
β(2nd β(πΌβππ½)))) β (πβ(2nd β(2nd
β(πΌβππ½))))}) |
36 | 24 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ ((πΌ β Ο β§ π½ β Ο) β
(2nd β(πΌβππ½)) = (2nd ββ¨β
,
β¨πΌ, π½β©β©)) |
37 | | opex 5426 |
. . . . . . . . . . . . . 14
β’
β¨πΌ, π½β© β V |
38 | 25, 37 | op2nd 7935 |
. . . . . . . . . . . . 13
β’
(2nd ββ¨β
, β¨πΌ, π½β©β©) = β¨πΌ, π½β© |
39 | 36, 38 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ ((πΌ β Ο β§ π½ β Ο) β
(2nd β(πΌβππ½)) = β¨πΌ, π½β©) |
40 | 39 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((πΌ β Ο β§ π½ β Ο) β
(1st β(2nd β(πΌβππ½))) = (1st ββ¨πΌ, π½β©)) |
41 | | op1stg 7938 |
. . . . . . . . . . 11
β’ ((πΌ β Ο β§ π½ β Ο) β
(1st ββ¨πΌ, π½β©) = πΌ) |
42 | 40, 41 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((πΌ β Ο β§ π½ β Ο) β
(1st β(2nd β(πΌβππ½))) = πΌ) |
43 | 42 | fveq2d 6851 |
. . . . . . . . 9
β’ ((πΌ β Ο β§ π½ β Ο) β (πβ(1st
β(2nd β(πΌβππ½)))) = (πβπΌ)) |
44 | 39 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((πΌ β Ο β§ π½ β Ο) β
(2nd β(2nd β(πΌβππ½))) = (2nd ββ¨πΌ, π½β©)) |
45 | | op2ndg 7939 |
. . . . . . . . . . 11
β’ ((πΌ β Ο β§ π½ β Ο) β
(2nd ββ¨πΌ, π½β©) = π½) |
46 | 44, 45 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((πΌ β Ο β§ π½ β Ο) β
(2nd β(2nd β(πΌβππ½))) = π½) |
47 | 46 | fveq2d 6851 |
. . . . . . . . 9
β’ ((πΌ β Ο β§ π½ β Ο) β (πβ(2nd
β(2nd β(πΌβππ½)))) = (πβπ½)) |
48 | 43, 47 | eleq12d 2832 |
. . . . . . . 8
β’ ((πΌ β Ο β§ π½ β Ο) β ((πβ(1st
β(2nd β(πΌβππ½)))) β (πβ(2nd β(2nd
β(πΌβππ½)))) β (πβπΌ) β (πβπ½))) |
49 | 48 | rabbidv 3418 |
. . . . . . 7
β’ ((πΌ β Ο β§ π½ β Ο) β {π β ({π} βm Ο) β£ (πβ(1st
β(2nd β(πΌβππ½)))) β (πβ(2nd β(2nd
β(πΌβππ½))))} = {π β ({π} βm Ο) β£ (πβπΌ) β (πβπ½)}) |
50 | 49 | 3adant3 1133 |
. . . . . 6
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β {π β ({π} βm Ο) β£ (πβ(1st
β(2nd β(πΌβππ½)))) β (πβ(2nd β(2nd
β(πΌβππ½))))} = {π β ({π} βm Ο) β£ (πβπΌ) β (πβπ½)}) |
51 | | elmapi 8794 |
. . . . . . . . . 10
β’ (π β ({π} βm Ο) β π:ΟβΆ{π}) |
52 | | elirr 9540 |
. . . . . . . . . . . 12
β’ Β¬
π β π |
53 | | fvconst 7115 |
. . . . . . . . . . . . . 14
β’ ((π:ΟβΆ{π} β§ πΌ β Ο) β (πβπΌ) = π) |
54 | 53 | 3ad2antr1 1189 |
. . . . . . . . . . . . 13
β’ ((π:ΟβΆ{π} β§ (πΌ β Ο β§ π½ β Ο β§ π β π)) β (πβπΌ) = π) |
55 | | fvconst 7115 |
. . . . . . . . . . . . . 14
β’ ((π:ΟβΆ{π} β§ π½ β Ο) β (πβπ½) = π) |
56 | 55 | 3ad2antr2 1190 |
. . . . . . . . . . . . 13
β’ ((π:ΟβΆ{π} β§ (πΌ β Ο β§ π½ β Ο β§ π β π)) β (πβπ½) = π) |
57 | 54, 56 | eleq12d 2832 |
. . . . . . . . . . . 12
β’ ((π:ΟβΆ{π} β§ (πΌ β Ο β§ π½ β Ο β§ π β π)) β ((πβπΌ) β (πβπ½) β π β π)) |
58 | 52, 57 | mtbiri 327 |
. . . . . . . . . . 11
β’ ((π:ΟβΆ{π} β§ (πΌ β Ο β§ π½ β Ο β§ π β π)) β Β¬ (πβπΌ) β (πβπ½)) |
59 | 58 | ex 414 |
. . . . . . . . . 10
β’ (π:ΟβΆ{π} β ((πΌ β Ο β§ π½ β Ο β§ π β π) β Β¬ (πβπΌ) β (πβπ½))) |
60 | 51, 59 | syl 17 |
. . . . . . . . 9
β’ (π β ({π} βm Ο) β ((πΌ β Ο β§ π½ β Ο β§ π β π) β Β¬ (πβπΌ) β (πβπ½))) |
61 | 60 | impcom 409 |
. . . . . . . 8
β’ (((πΌ β Ο β§ π½ β Ο β§ π β π) β§ π β ({π} βm Ο)) β Β¬
(πβπΌ) β (πβπ½)) |
62 | 61 | ralrimiva 3144 |
. . . . . . 7
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β βπ β ({π} βm Ο) Β¬ (πβπΌ) β (πβπ½)) |
63 | | rabeq0 4349 |
. . . . . . 7
β’ ({π β ({π} βm Ο) β£ (πβπΌ) β (πβπ½)} = β
β βπ β ({π} βm Ο) Β¬ (πβπΌ) β (πβπ½)) |
64 | 62, 63 | sylibr 233 |
. . . . . 6
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β {π β ({π} βm Ο) β£ (πβπΌ) β (πβπ½)} = β
) |
65 | 50, 64 | eqtrd 2777 |
. . . . 5
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β {π β ({π} βm Ο) β£ (πβ(1st
β(2nd β(πΌβππ½)))) β (πβ(2nd β(2nd
β(πΌβππ½))))} = β
) |
66 | 35, 65 | eqtrd 2777 |
. . . 4
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β ({π} Satβ (πΌβππ½)) = β
) |
67 | 66 | eqeq1d 2739 |
. . 3
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β (({π} Satβ (πΌβππ½)) = ({π} βm Ο) β β
= ({π} βm
Ο))) |
68 | 23, 67 | bitrd 279 |
. 2
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β ({π}β§(πΌβππ½) β β
= ({π} βm
Ο))) |
69 | 19, 68 | mtbird 325 |
1
β’ ((πΌ β Ο β§ π½ β Ο β§ π β π) β Β¬ {π}β§(πΌβππ½)) |