Step | Hyp | Ref
| Expression |
1 | | fmla0 34442 |
. . . 4
β’
(Fmlaββ
) = {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
2 | | rabab 3502 |
. . . 4
β’ {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} = {π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
3 | 1, 2 | eqtri 2760 |
. . 3
β’
(Fmlaββ
) = {π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
4 | 3 | ineq1i 4208 |
. 2
β’
((Fmlaββ
) β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = ({π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) |
5 | | inab 4299 |
. . 3
β’ ({π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = {π₯ β£ (βπ β Ο βπ β Ο π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))} |
6 | | goel 34407 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ π β Ο) β (πβππ) = β¨β
, β¨π, πβ©β©) |
7 | 6 | eqeq2d 2743 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β π₯ = β¨β
, β¨π, πβ©β©)) |
8 | | 1n0 8490 |
. . . . . . . . . . . . . . . . . . . 20
β’
1o β β
|
9 | 8 | nesymi 2998 |
. . . . . . . . . . . . . . . . . . 19
β’ Β¬
β
= 1o |
10 | 9 | intnanr 488 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬
(β
= 1o β§ β¨π, πβ© = β¨π’, π£β©) |
11 | | gonafv 34410 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π’ β V β§ π£ β V) β (π’βΌππ£) = β¨1o,
β¨π’, π£β©β©) |
12 | 11 | el2v 3482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π’βΌππ£) = β¨1o,
β¨π’, π£β©β© |
13 | 12 | eqeq2i 2745 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β
, β¨π, πβ©β© = (π’βΌππ£) β β¨β
, β¨π, πβ©β© = β¨1o,
β¨π’, π£β©β©) |
14 | | 0ex 5307 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β V |
15 | | opex 5464 |
. . . . . . . . . . . . . . . . . . . 20
β’
β¨π, πβ© β V |
16 | 14, 15 | opth 5476 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β
, β¨π, πβ©β© = β¨1o,
β¨π’, π£β©β© β (β
= 1o
β§ β¨π, πβ© = β¨π’, π£β©)) |
17 | 13, 16 | bitri 274 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨β
, β¨π, πβ©β© = (π’βΌππ£) β (β
= 1o β§
β¨π, πβ© = β¨π’, π£β©)) |
18 | 10, 17 | mtbir 322 |
. . . . . . . . . . . . . . . . 17
β’ Β¬
β¨β
, β¨π,
πβ©β© = (π’βΌππ£) |
19 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = β¨β
, β¨π, πβ©β© β (π₯ = (π’βΌππ£) β β¨β
, β¨π, πβ©β© = (π’βΌππ£))) |
20 | 18, 19 | mtbiri 326 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = β¨β
, β¨π, πβ©β© β Β¬ π₯ = (π’βΌππ£)) |
21 | 7, 20 | syl6bi 252 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β Β¬ π₯ = (π’βΌππ£))) |
22 | 21 | imp 407 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β Β¬ π₯ = (π’βΌππ£)) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β Β¬
π₯ = (π’βΌππ£)) |
24 | 23 | ralrimivw 3150 |
. . . . . . . . . . . 12
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β
βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£)) |
25 | | 2on0 8484 |
. . . . . . . . . . . . . . . . . . . . 21
β’
2o β β
|
26 | 25 | nesymi 2998 |
. . . . . . . . . . . . . . . . . . . 20
β’ Β¬
β
= 2o |
27 | 26 | orci 863 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
β
= 2o β¨ Β¬ β¨π, πβ© = β¨π, π’β©) |
28 | 14, 15 | opth 5476 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨β
, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β© β (β
= 2o
β§ β¨π, πβ© = β¨π, π’β©)) |
29 | 28 | notbii 319 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
β¨β
, β¨π,
πβ©β© =
β¨2o, β¨π, π’β©β© β Β¬ (β
=
2o β§ β¨π, πβ© = β¨π, π’β©)) |
30 | | ianor 980 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
(β
= 2o β§ β¨π, πβ© = β¨π, π’β©) β (Β¬ β
= 2o
β¨ Β¬ β¨π, πβ© = β¨π, π’β©)) |
31 | 29, 30 | bitri 274 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
β¨β
, β¨π,
πβ©β© =
β¨2o, β¨π, π’β©β© β (Β¬ β
=
2o β¨ Β¬ β¨π, πβ© = β¨π, π’β©)) |
32 | 27, 31 | mpbir 230 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬
β¨β
, β¨π,
πβ©β© =
β¨2o, β¨π, π’β©β© |
33 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = β¨β
, β¨π, πβ©β© β (π₯ = βπππ’ β β¨β
, β¨π, πβ©β© =
βπππ’)) |
34 | | df-goal 34402 |
. . . . . . . . . . . . . . . . . . . 20
β’
βπππ’ = β¨2o, β¨π, π’β©β© |
35 | 34 | eqeq2i 2745 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β
, β¨π, πβ©β© =
βπππ’ β β¨β
, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β©) |
36 | 33, 35 | bitrdi 286 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = β¨β
, β¨π, πβ©β© β (π₯ = βπππ’ β β¨β
, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β©)) |
37 | 32, 36 | mtbiri 326 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = β¨β
, β¨π, πβ©β© β Β¬ π₯ = βπππ’) |
38 | 7, 37 | syl6bi 252 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β Β¬ π₯ = βπππ’)) |
39 | 38 | imp 407 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β Β¬ π₯ = βπππ’) |
40 | 39 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β Β¬
π₯ =
βπππ’) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . 13
β’
(((((π β
Ο β§ π β
Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β§ π β Ο) β Β¬
π₯ =
βπππ’) |
42 | 41 | ralrimiva 3146 |
. . . . . . . . . . . 12
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β
βπ β Ο
Β¬ π₯ =
βπππ’) |
43 | 24, 42 | jca 512 |
. . . . . . . . . . 11
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β
(βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’)) |
44 | 43 | ralrimiva 3146 |
. . . . . . . . . 10
β’ (((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β βπ’ β (Fmlaββ
)(βπ£ β (Fmlaββ
)
Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ =
βπππ’)) |
45 | | ralnex 3072 |
. . . . . . . . . . . . . 14
β’
(βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β Β¬ βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£)) |
46 | | ralnex 3072 |
. . . . . . . . . . . . . 14
β’
(βπ β
Ο Β¬ π₯ =
βπππ’ β Β¬ βπ β Ο π₯ = βπππ’) |
47 | 45, 46 | anbi12i 627 |
. . . . . . . . . . . . 13
β’
((βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’) β (Β¬ βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β§ Β¬ βπ β Ο π₯ = βπππ’)) |
48 | | ioran 982 |
. . . . . . . . . . . . 13
β’ (Β¬
(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’) β (Β¬ βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β§ Β¬ βπ β Ο π₯ = βπππ’)) |
49 | 47, 48 | bitr4i 277 |
. . . . . . . . . . . 12
β’
((βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’) β Β¬ (βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
50 | 49 | ralbii 3093 |
. . . . . . . . . . 11
β’
(βπ’ β
(Fmlaββ
)(βπ£ β (Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’) β βπ’ β (Fmlaββ
) Β¬
(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
51 | | ralnex 3072 |
. . . . . . . . . . 11
β’
(βπ’ β
(Fmlaββ
) Β¬ (βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’) β Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
52 | 50, 51 | bitri 274 |
. . . . . . . . . 10
β’
(βπ’ β
(Fmlaββ
)(βπ£ β (Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’) β Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
53 | 44, 52 | sylib 217 |
. . . . . . . . 9
β’ (((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
54 | 53 | ex 413 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))) |
55 | 54 | rexlimdva 3155 |
. . . . . . 7
β’ (π β Ο β
(βπ β Ο
π₯ = (πβππ) β Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))) |
56 | 55 | rexlimiv 3148 |
. . . . . 6
β’
(βπ β
Ο βπ β
Ο π₯ = (πβππ) β Β¬ βπ’ β
(Fmlaββ
)(βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
57 | 56 | imori 852 |
. . . . 5
β’ (Β¬
βπ β Ο
βπ β Ο
π₯ = (πβππ) β¨ Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
58 | | ianor 980 |
. . . . 5
β’ (Β¬
(βπ β Ο
βπ β Ο
π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) β (Β¬ βπ β Ο βπ β Ο π₯ = (πβππ) β¨ Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))) |
59 | 57, 58 | mpbir 230 |
. . . 4
β’ Β¬
(βπ β Ο
βπ β Ο
π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
60 | 59 | abf 4402 |
. . 3
β’ {π₯ β£ (βπ β Ο βπ β Ο π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))} = β
|
61 | 5, 60 | eqtri 2760 |
. 2
β’ ({π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = β
|
62 | 4, 61 | eqtri 2760 |
1
β’
((Fmlaββ
) β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = β
|