Step | Hyp | Ref
| Expression |
1 | | df-goal 34328 |
. . . 4
β’
βπππ΄ = β¨2o, β¨π, π΄β©β© |
2 | | 2on0 8481 |
. . . . . . . . . . . 12
β’
2o β β
|
3 | 2 | neii 2942 |
. . . . . . . . . . 11
β’ Β¬
2o = β
|
4 | 3 | intnanr 488 |
. . . . . . . . . 10
β’ Β¬
(2o = β
β§ β¨π, π΄β© = β¨π, πβ©) |
5 | | 2oex 8476 |
. . . . . . . . . . 11
β’
2o β V |
6 | | opex 5464 |
. . . . . . . . . . 11
β’
β¨π, π΄β© β V |
7 | 5, 6 | opth 5476 |
. . . . . . . . . 10
β’
(β¨2o, β¨π, π΄β©β© = β¨β
, β¨π, πβ©β© β (2o = β
β§ β¨π, π΄β© = β¨π, πβ©)) |
8 | 4, 7 | mtbir 322 |
. . . . . . . . 9
β’ Β¬
β¨2o, β¨π, π΄β©β© = β¨β
, β¨π, πβ©β© |
9 | | goel 34333 |
. . . . . . . . . 10
β’ ((π β Ο β§ π β Ο) β (πβππ) = β¨β
, β¨π, πβ©β©) |
10 | 9 | eqeq2d 2743 |
. . . . . . . . 9
β’ ((π β Ο β§ π β Ο) β
(β¨2o, β¨π, π΄β©β© = (πβππ) β β¨2o, β¨π, π΄β©β© = β¨β
, β¨π, πβ©β©)) |
11 | 8, 10 | mtbiri 326 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β Β¬
β¨2o, β¨π, π΄β©β© = (πβππ)) |
12 | 11 | rgen2 3197 |
. . . . . . 7
β’
βπ β
Ο βπ β
Ο Β¬ β¨2o, β¨π, π΄β©β© = (πβππ) |
13 | | ralnex2 3133 |
. . . . . . 7
β’
(βπ β
Ο βπ β
Ο Β¬ β¨2o, β¨π, π΄β©β© = (πβππ) β Β¬ βπ β Ο βπ β Ο β¨2o,
β¨π, π΄β©β© = (πβππ)) |
14 | 12, 13 | mpbi 229 |
. . . . . 6
β’ Β¬
βπ β Ο
βπ β Ο
β¨2o, β¨π, π΄β©β© = (πβππ) |
15 | 14 | intnan 487 |
. . . . 5
β’ Β¬
(β¨2o, β¨π, π΄β©β© β V β§ βπ β Ο βπ β Ο
β¨2o, β¨π, π΄β©β© = (πβππ)) |
16 | | eqeq1 2736 |
. . . . . . 7
β’ (π₯ = β¨2o,
β¨π, π΄β©β© β (π₯ = (πβππ) β β¨2o, β¨π, π΄β©β© = (πβππ))) |
17 | 16 | 2rexbidv 3219 |
. . . . . 6
β’ (π₯ = β¨2o,
β¨π, π΄β©β© β (βπ β Ο βπ β Ο π₯ = (πβππ) β βπ β Ο βπ β Ο β¨2o,
β¨π, π΄β©β© = (πβππ))) |
18 | | fmla0 34368 |
. . . . . 6
β’
(Fmlaββ
) = {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
19 | 17, 18 | elrab2 3686 |
. . . . 5
β’
(β¨2o, β¨π, π΄β©β© β (Fmlaββ
)
β (β¨2o, β¨π, π΄β©β© β V β§ βπ β Ο βπ β Ο
β¨2o, β¨π, π΄β©β© = (πβππ))) |
20 | 15, 19 | mtbir 322 |
. . . 4
β’ Β¬
β¨2o, β¨π, π΄β©β© β
(Fmlaββ
) |
21 | 1, 20 | eqneltri 2852 |
. . 3
β’ Β¬
βπππ΄ β
(Fmlaββ
) |
22 | | fveq2 6891 |
. . . 4
β’ (π = β
β
(Fmlaβπ) =
(Fmlaββ
)) |
23 | 22 | eleq2d 2819 |
. . 3
β’ (π = β
β
(βπππ΄ β (Fmlaβπ) β βπππ΄ β
(Fmlaββ
))) |
24 | 21, 23 | mtbiri 326 |
. 2
β’ (π = β
β Β¬
βπππ΄ β (Fmlaβπ)) |
25 | 24 | necon2ai 2970 |
1
β’
(βπππ΄ β (Fmlaβπ) β π β β
) |