Step | Hyp | Ref
| Expression |
1 | | fmla0 34668 |
. . . 4
β’
(Fmlaββ
) = {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
2 | | rabab 3502 |
. . . 4
β’ {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} = {π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
3 | 1, 2 | eqtri 2759 |
. . 3
β’
(Fmlaββ
) = {π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
4 | 3 | ineq1i 4209 |
. 2
β’
((Fmlaββ
) β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = ({π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) |
5 | | inab 4300 |
. . 3
β’ ({π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = {π₯ β£ (βπ β Ο βπ β Ο π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))} |
6 | | goel 34633 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ π β Ο) β (πβππ) = β¨β
, β¨π, πβ©β©) |
7 | 6 | eqeq2d 2742 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β π₯ = β¨β
, β¨π, πβ©β©)) |
8 | | 1n0 8491 |
. . . . . . . . . . . . . . . . . . . 20
β’
1o β β
|
9 | 8 | nesymi 2997 |
. . . . . . . . . . . . . . . . . . 19
β’ Β¬
β
= 1o |
10 | 9 | intnanr 487 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬
(β
= 1o β§ β¨π, πβ© = β¨π’, π£β©) |
11 | | gonafv 34636 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π’ β V β§ π£ β V) β (π’βΌππ£) = β¨1o,
β¨π’, π£β©β©) |
12 | 11 | el2v 3481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π’βΌππ£) = β¨1o,
β¨π’, π£β©β© |
13 | 12 | eqeq2i 2744 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β
, β¨π, πβ©β© = (π’βΌππ£) β β¨β
, β¨π, πβ©β© = β¨1o,
β¨π’, π£β©β©) |
14 | | 0ex 5308 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β V |
15 | | opex 5465 |
. . . . . . . . . . . . . . . . . . . 20
β’
β¨π, πβ© β V |
16 | 14, 15 | opth 5477 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β
, β¨π, πβ©β© = β¨1o,
β¨π’, π£β©β© β (β
= 1o
β§ β¨π, πβ© = β¨π’, π£β©)) |
17 | 13, 16 | bitri 274 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨β
, β¨π, πβ©β© = (π’βΌππ£) β (β
= 1o β§
β¨π, πβ© = β¨π’, π£β©)) |
18 | 10, 17 | mtbir 322 |
. . . . . . . . . . . . . . . . 17
β’ Β¬
β¨β
, β¨π,
πβ©β© = (π’βΌππ£) |
19 | | eqeq1 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = β¨β
, β¨π, πβ©β© β (π₯ = (π’βΌππ£) β β¨β
, β¨π, πβ©β© = (π’βΌππ£))) |
20 | 18, 19 | mtbiri 326 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = β¨β
, β¨π, πβ©β© β Β¬ π₯ = (π’βΌππ£)) |
21 | 7, 20 | syl6bi 252 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β Β¬ π₯ = (π’βΌππ£))) |
22 | 21 | imp 406 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β Β¬ π₯ = (π’βΌππ£)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β Β¬
π₯ = (π’βΌππ£)) |
24 | 23 | ralrimivw 3149 |
. . . . . . . . . . . 12
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β
βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£)) |
25 | | 2on0 8485 |
. . . . . . . . . . . . . . . . . . . . 21
β’
2o β β
|
26 | 25 | nesymi 2997 |
. . . . . . . . . . . . . . . . . . . 20
β’ Β¬
β
= 2o |
27 | 26 | orci 862 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
β
= 2o β¨ Β¬ β¨π, πβ© = β¨π, π’β©) |
28 | 14, 15 | opth 5477 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨β
, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β© β (β
= 2o
β§ β¨π, πβ© = β¨π, π’β©)) |
29 | 28 | notbii 319 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
β¨β
, β¨π,
πβ©β© =
β¨2o, β¨π, π’β©β© β Β¬ (β
=
2o β§ β¨π, πβ© = β¨π, π’β©)) |
30 | | ianor 979 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
(β
= 2o β§ β¨π, πβ© = β¨π, π’β©) β (Β¬ β
= 2o
β¨ Β¬ β¨π, πβ© = β¨π, π’β©)) |
31 | 29, 30 | bitri 274 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
β¨β
, β¨π,
πβ©β© =
β¨2o, β¨π, π’β©β© β (Β¬ β
=
2o β¨ Β¬ β¨π, πβ© = β¨π, π’β©)) |
32 | 27, 31 | mpbir 230 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬
β¨β
, β¨π,
πβ©β© =
β¨2o, β¨π, π’β©β© |
33 | | eqeq1 2735 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = β¨β
, β¨π, πβ©β© β (π₯ = βπππ’ β β¨β
, β¨π, πβ©β© =
βπππ’)) |
34 | | df-goal 34628 |
. . . . . . . . . . . . . . . . . . . 20
β’
βπππ’ = β¨2o, β¨π, π’β©β© |
35 | 34 | eqeq2i 2744 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β
, β¨π, πβ©β© =
βπππ’ β β¨β
, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β©) |
36 | 33, 35 | bitrdi 286 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = β¨β
, β¨π, πβ©β© β (π₯ = βπππ’ β β¨β
, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β©)) |
37 | 32, 36 | mtbiri 326 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = β¨β
, β¨π, πβ©β© β Β¬ π₯ = βπππ’) |
38 | 7, 37 | syl6bi 252 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β Β¬ π₯ = βπππ’)) |
39 | 38 | imp 406 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β Β¬ π₯ = βπππ’) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β Β¬
π₯ =
βπππ’) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . 13
β’
(((((π β
Ο β§ π β
Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β§ π β Ο) β Β¬
π₯ =
βπππ’) |
42 | 41 | ralrimiva 3145 |
. . . . . . . . . . . 12
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β
βπ β Ο
Β¬ π₯ =
βπππ’) |
43 | 24, 42 | jca 511 |
. . . . . . . . . . 11
β’ ((((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β§ π’ β (Fmlaββ
)) β
(βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’)) |
44 | 43 | ralrimiva 3145 |
. . . . . . . . . 10
β’ (((π β Ο β§ π β Ο) β§ π₯ = (πβππ)) β βπ’ β (Fmlaββ
)(βπ£ β (Fmlaββ
)
Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ =
βπππ’)) |
45 | | ralnex 3071 |
. . . . . . . . . . . . . 14
β’
(βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β Β¬ βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£)) |
46 | | ralnex 3071 |
. . . . . . . . . . . . . 14
β’
(βπ β
Ο Β¬ π₯ =
βπππ’ β Β¬ βπ β Ο π₯ = βπππ’) |
47 | 45, 46 | anbi12i 626 |
. . . . . . . . . . . . 13
β’
((βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’) β (Β¬ βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β§ Β¬ βπ β Ο π₯ = βπππ’)) |
48 | | ioran 981 |
. . . . . . . . . . . . 13
β’ (Β¬
(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’) β (Β¬ βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β§ Β¬ βπ β Ο π₯ = βπππ’)) |
49 | 47, 48 | bitr4i 277 |
. . . . . . . . . . . 12
β’
((βπ£ β
(Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’) β Β¬ (βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
50 | 49 | ralbii 3092 |
. . . . . . . . . . 11
β’
(βπ’ β
(Fmlaββ
)(βπ£ β (Fmlaββ
) Β¬ π₯ = (π’βΌππ£) β§ βπ β Ο Β¬ π₯ = βπππ’) β βπ’ β (Fmlaββ
) Β¬
(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
51 | | ralnex 3071 |
. . . . . . . . . . 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 412 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β (π₯ = (πβππ) β Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))) |
55 | 54 | rexlimdva 3154 |
. . . . . . 7
β’ (π β Ο β
(βπ β Ο
π₯ = (πβππ) β Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))) |
56 | 55 | rexlimiv 3147 |
. . . . . 6
β’
(βπ β
Ο βπ β
Ο π₯ = (πβππ) β Β¬ βπ’ β
(Fmlaββ
)(βπ£ β (Fmlaββ
)π₯ = (π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
57 | 56 | imori 851 |
. . . . 5
β’ (Β¬
βπ β Ο
βπ β Ο
π₯ = (πβππ) β¨ Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
58 | | ianor 979 |
. . . . 5
β’ (Β¬
(βπ β Ο
βπ β Ο
π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) β (Β¬ βπ β Ο βπ β Ο π₯ = (πβππ) β¨ Β¬ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))) |
59 | 57, 58 | mpbir 230 |
. . . 4
β’ Β¬
(βπ β Ο
βπ β Ο
π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)) |
60 | 59 | abf 4403 |
. . 3
β’ {π₯ β£ (βπ β Ο βπ β Ο π₯ = (πβππ) β§ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’))} = β
|
61 | 5, 60 | eqtri 2759 |
. 2
β’ ({π₯ β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = β
|
62 | 4, 61 | eqtri 2759 |
1
β’
((Fmlaββ
) β© {π₯ β£ βπ’ β (Fmlaββ
)(βπ£ β
(Fmlaββ
)π₯ =
(π’βΌππ£) β¨ βπ β Ο π₯ = βπππ’)}) = β
|