Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = β
β
(Fmlaβπ₯) =
(Fmlaββ
)) |
2 | 1 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = β
β (πΉ β (Fmlaβπ₯) β πΉ β
(Fmlaββ
))) |
3 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = β
β ((β
Sat
β
)βπ₯) =
((β
Sat β
)ββ
)) |
4 | 3 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = β
β (β¨πΉ, β
β© β ((β
Sat β
)βπ₯)
β β¨πΉ,
β
β© β ((β
Sat β
)ββ
))) |
5 | 2, 4 | bibi12d 345 |
. . . . 5
β’ (π₯ = β
β ((πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯)) β
(πΉ β
(Fmlaββ
) β β¨πΉ, β
β© β ((β
Sat
β
)ββ
)))) |
6 | 5 | imbi2d 340 |
. . . 4
β’ (π₯ = β
β ((πΉ β V β (πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯))) β
(πΉ β V β (πΉ β (Fmlaββ
)
β β¨πΉ,
β
β© β ((β
Sat β
)ββ
))))) |
7 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π¦ β (Fmlaβπ₯) = (Fmlaβπ¦)) |
8 | 7 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = π¦ β (πΉ β (Fmlaβπ₯) β πΉ β (Fmlaβπ¦))) |
9 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π¦ β ((β
Sat β
)βπ₯) = ((β
Sat
β
)βπ¦)) |
10 | 9 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = π¦ β (β¨πΉ, β
β© β ((β
Sat
β
)βπ₯) β
β¨πΉ, β
β©
β ((β
Sat β
)βπ¦))) |
11 | 8, 10 | bibi12d 345 |
. . . . 5
β’ (π₯ = π¦ β ((πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯)) β
(πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) |
12 | 11 | imbi2d 340 |
. . . 4
β’ (π₯ = π¦ β ((πΉ β V β (πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯))) β
(πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦))))) |
13 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = suc π¦ β (Fmlaβπ₯) = (Fmlaβsuc π¦)) |
14 | 13 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = suc π¦ β (πΉ β (Fmlaβπ₯) β πΉ β (Fmlaβsuc π¦))) |
15 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = suc π¦ β ((β
Sat β
)βπ₯) = ((β
Sat
β
)βsuc π¦)) |
16 | 15 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = suc π¦ β (β¨πΉ, β
β© β ((β
Sat
β
)βπ₯) β
β¨πΉ, β
β©
β ((β
Sat β
)βsuc π¦))) |
17 | 14, 16 | bibi12d 345 |
. . . . 5
β’ (π₯ = suc π¦ β ((πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯)) β
(πΉ β (Fmlaβsuc
π¦) β β¨πΉ, β
β© β ((β
Sat β
)βsuc π¦)))) |
18 | 17 | imbi2d 340 |
. . . 4
β’ (π₯ = suc π¦ β ((πΉ β V β (πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯))) β
(πΉ β V β (πΉ β (Fmlaβsuc π¦) β β¨πΉ, β
β© β ((β
Sat
β
)βsuc π¦))))) |
19 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π β (Fmlaβπ₯) = (Fmlaβπ)) |
20 | 19 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = π β (πΉ β (Fmlaβπ₯) β πΉ β (Fmlaβπ))) |
21 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π β ((β
Sat β
)βπ₯) = ((β
Sat
β
)βπ)) |
22 | 21 | eleq2d 2819 |
. . . . . 6
β’ (π₯ = π β (β¨πΉ, β
β© β ((β
Sat
β
)βπ₯) β
β¨πΉ, β
β©
β ((β
Sat β
)βπ))) |
23 | 20, 22 | bibi12d 345 |
. . . . 5
β’ (π₯ = π β ((πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯)) β
(πΉ β (Fmlaβπ) β β¨πΉ, β
β© β ((β
Sat
β
)βπ)))) |
24 | 23 | imbi2d 340 |
. . . 4
β’ (π₯ = π β ((πΉ β V β (πΉ β (Fmlaβπ₯) β β¨πΉ, β
β© β ((β
Sat
β
)βπ₯))) β
(πΉ β V β (πΉ β (Fmlaβπ) β β¨πΉ, β
β© β ((β
Sat
β
)βπ))))) |
25 | | eqeq1 2736 |
. . . . . . . 8
β’ (π₯ = πΉ β (π₯ = (πβππ) β πΉ = (πβππ))) |
26 | 25 | 2rexbidv 3219 |
. . . . . . 7
β’ (π₯ = πΉ β (βπ β Ο βπ β Ο π₯ = (πβππ) β βπ β Ο βπ β Ο πΉ = (πβππ))) |
27 | 26 | elrab 3683 |
. . . . . 6
β’ (πΉ β {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β (πΉ β V β§ βπ β Ο βπ β Ο πΉ = (πβππ))) |
28 | | eqidd 2733 |
. . . . . . . 8
β’ ((πΉ β V β§ βπ β Ο βπ β Ο πΉ = (πβππ)) β β
= β
) |
29 | | simpr 485 |
. . . . . . . 8
β’ ((πΉ β V β§ βπ β Ο βπ β Ο πΉ = (πβππ)) β βπ β Ο βπ β Ο πΉ = (πβππ)) |
30 | 28, 29 | jca 512 |
. . . . . . 7
β’ ((πΉ β V β§ βπ β Ο βπ β Ο πΉ = (πβππ)) β (β
= β
β§
βπ β Ο
βπ β Ο
πΉ = (πβππ))) |
31 | | simpr 485 |
. . . . . . . . 9
β’ ((β
= β
β§ βπ
β Ο βπ
β Ο πΉ = (πβππ)) β βπ β Ο βπ β Ο πΉ = (πβππ)) |
32 | 31 | anim2i 617 |
. . . . . . . 8
β’ ((πΉ β V β§ (β
=
β
β§ βπ
β Ο βπ
β Ο πΉ = (πβππ))) β (πΉ β V β§ βπ β Ο βπ β Ο πΉ = (πβππ))) |
33 | 32 | ex 413 |
. . . . . . 7
β’ (πΉ β V β ((β
=
β
β§ βπ
β Ο βπ
β Ο πΉ = (πβππ)) β (πΉ β V β§ βπ β Ο βπ β Ο πΉ = (πβππ)))) |
34 | 30, 33 | impbid2 225 |
. . . . . 6
β’ (πΉ β V β ((πΉ β V β§ βπ β Ο βπ β Ο πΉ = (πβππ)) β (β
= β
β§
βπ β Ο
βπ β Ο
πΉ = (πβππ)))) |
35 | 27, 34 | bitrid 282 |
. . . . 5
β’ (πΉ β V β (πΉ β {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β (β
= β
β§
βπ β Ο
βπ β Ο
πΉ = (πβππ)))) |
36 | | fmla0 34442 |
. . . . . . 7
β’
(Fmlaββ
) = {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
37 | 36 | eleq2i 2825 |
. . . . . 6
β’ (πΉ β (Fmlaββ
)
β πΉ β {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)}) |
38 | 37 | a1i 11 |
. . . . 5
β’ (πΉ β V β (πΉ β (Fmlaββ
)
β πΉ β {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)})) |
39 | | satf00 34434 |
. . . . . . . 8
β’ ((β
Sat β
)ββ
) = {β¨π₯, π¦β© β£ (π¦ = β
β§ βπ β Ο βπ β Ο π₯ = (πβππ))} |
40 | 39 | a1i 11 |
. . . . . . 7
β’ (πΉ β V β ((β
Sat
β
)ββ
) = {β¨π₯, π¦β© β£ (π¦ = β
β§ βπ β Ο βπ β Ο π₯ = (πβππ))}) |
41 | 40 | eleq2d 2819 |
. . . . . 6
β’ (πΉ β V β (β¨πΉ, β
β© β ((β
Sat β
)ββ
) β β¨πΉ, β
β© β {β¨π₯, π¦β© β£ (π¦ = β
β§ βπ β Ο βπ β Ο π₯ = (πβππ))})) |
42 | | 0ex 5307 |
. . . . . . 7
β’ β
β V |
43 | | eqeq1 2736 |
. . . . . . . . 9
β’ (π¦ = β
β (π¦ = β
β β
=
β
)) |
44 | 43, 26 | bi2anan9r 638 |
. . . . . . . 8
β’ ((π₯ = πΉ β§ π¦ = β
) β ((π¦ = β
β§ βπ β Ο βπ β Ο π₯ = (πβππ)) β (β
= β
β§
βπ β Ο
βπ β Ο
πΉ = (πβππ)))) |
45 | 44 | opelopabga 5533 |
. . . . . . 7
β’ ((πΉ β V β§ β
β
V) β (β¨πΉ,
β
β© β {β¨π₯, π¦β© β£ (π¦ = β
β§ βπ β Ο βπ β Ο π₯ = (πβππ))} β (β
= β
β§
βπ β Ο
βπ β Ο
πΉ = (πβππ)))) |
46 | 42, 45 | mpan2 689 |
. . . . . 6
β’ (πΉ β V β (β¨πΉ, β
β© β
{β¨π₯, π¦β© β£ (π¦ = β
β§ βπ β Ο βπ β Ο π₯ = (πβππ))} β (β
= β
β§
βπ β Ο
βπ β Ο
πΉ = (πβππ)))) |
47 | 41, 46 | bitrd 278 |
. . . . 5
β’ (πΉ β V β (β¨πΉ, β
β© β ((β
Sat β
)ββ
) β (β
= β
β§ βπ β Ο βπ β Ο πΉ = (πβππ)))) |
48 | 35, 38, 47 | 3bitr4d 310 |
. . . 4
β’ (πΉ β V β (πΉ β (Fmlaββ
)
β β¨πΉ,
β
β© β ((β
Sat β
)ββ
))) |
49 | | eqid 2732 |
. . . . . . . . . . . 12
β’ β
=
β
|
50 | 49 | biantrur 531 |
. . . . . . . . . . 11
β’
(βπ’ β
((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’)) β (β
= β
β§
βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’)))) |
51 | 50 | bicomi 223 |
. . . . . . . . . 10
β’ ((β
= β
β§ βπ’
β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’))) β βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’))) |
52 | 51 | a1i 11 |
. . . . . . . . 9
β’ (πΉ β V β ((β
=
β
β§ βπ’
β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’))) β βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’)))) |
53 | | eqeq1 2736 |
. . . . . . . . . . . 12
β’ (π§ = β
β (π§ = β
β β
=
β
)) |
54 | | eqeq1 2736 |
. . . . . . . . . . . . . . 15
β’ (π₯ = πΉ β (π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β πΉ = ((1st βπ’)βΌπ(1st
βπ£)))) |
55 | 54 | rexbidv 3178 |
. . . . . . . . . . . . . 14
β’ (π₯ = πΉ β (βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β
βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)))) |
56 | | eqeq1 2736 |
. . . . . . . . . . . . . . 15
β’ (π₯ = πΉ β (π₯ = βππ(1st βπ’) β πΉ = βππ(1st βπ’))) |
57 | 56 | rexbidv 3178 |
. . . . . . . . . . . . . 14
β’ (π₯ = πΉ β (βπ β Ο π₯ = βππ(1st βπ’) β βπ β Ο πΉ =
βππ(1st βπ’))) |
58 | 55, 57 | orbi12d 917 |
. . . . . . . . . . . . 13
β’ (π₯ = πΉ β ((βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β (βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’)))) |
59 | 58 | rexbidv 3178 |
. . . . . . . . . . . 12
β’ (π₯ = πΉ β (βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’)))) |
60 | 53, 59 | bi2anan9r 638 |
. . . . . . . . . . 11
β’ ((π₯ = πΉ β§ π§ = β
) β ((π§ = β
β§ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β (β
= β
β§
βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’))))) |
61 | 60 | opelopabga 5533 |
. . . . . . . . . 10
β’ ((πΉ β V β§ β
β
V) β (β¨πΉ,
β
β© β {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))} β (β
= β
β§
βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’))))) |
62 | 42, 61 | mpan2 689 |
. . . . . . . . 9
β’ (πΉ β V β (β¨πΉ, β
β© β
{β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))} β (β
= β
β§
βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’))))) |
63 | 59 | elabg 3666 |
. . . . . . . . 9
β’ (πΉ β V β (πΉ β {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))} β βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)πΉ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
πΉ =
βππ(1st βπ’)))) |
64 | 52, 62, 63 | 3bitr4d 310 |
. . . . . . . 8
β’ (πΉ β V β (β¨πΉ, β
β© β
{β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))} β πΉ β {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))})) |
65 | 64 | adantl 482 |
. . . . . . 7
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β
(β¨πΉ, β
β©
β {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))} β πΉ β {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))})) |
66 | 65 | orbi2d 914 |
. . . . . 6
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β
((β¨πΉ, β
β©
β ((β
Sat β
)βπ¦) β¨ β¨πΉ, β
β© β {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))}) β (β¨πΉ, β
β© β ((β
Sat
β
)βπ¦) β¨
πΉ β {π₯ β£ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}))) |
67 | | eqid 2732 |
. . . . . . . . . 10
β’ (β
Sat β
) = (β
Sat β
) |
68 | 67 | satf0suc 34436 |
. . . . . . . . 9
β’ (π¦ β Ο β ((β
Sat β
)βsuc π¦) =
(((β
Sat β
)βπ¦) βͺ {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))})) |
69 | 68 | eleq2d 2819 |
. . . . . . . 8
β’ (π¦ β Ο β
(β¨πΉ, β
β©
β ((β
Sat β
)βsuc π¦) β β¨πΉ, β
β© β (((β
Sat
β
)βπ¦) βͺ
{β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))}))) |
70 | | elun 4148 |
. . . . . . . 8
β’
(β¨πΉ,
β
β© β (((β
Sat β
)βπ¦) βͺ {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))}) β (β¨πΉ, β
β© β ((β
Sat
β
)βπ¦) β¨
β¨πΉ, β
β©
β {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))})) |
71 | 69, 70 | bitrdi 286 |
. . . . . . 7
β’ (π¦ β Ο β
(β¨πΉ, β
β©
β ((β
Sat β
)βsuc π¦) β (β¨πΉ, β
β© β ((β
Sat
β
)βπ¦) β¨
β¨πΉ, β
β©
β {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))}))) |
72 | 71 | ad2antrr 724 |
. . . . . 6
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β
(β¨πΉ, β
β©
β ((β
Sat β
)βsuc π¦) β (β¨πΉ, β
β© β ((β
Sat
β
)βπ¦) β¨
β¨πΉ, β
β©
β {β¨π₯, π§β© β£ (π§ = β
β§ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))}))) |
73 | | fmlasuc0 34444 |
. . . . . . . . 9
β’ (π¦ β Ο β
(Fmlaβsuc π¦) =
((Fmlaβπ¦) βͺ
{π₯ β£ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))})) |
74 | 73 | eleq2d 2819 |
. . . . . . . 8
β’ (π¦ β Ο β (πΉ β (Fmlaβsuc π¦) β πΉ β ((Fmlaβπ¦) βͺ {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}))) |
75 | 74 | ad2antrr 724 |
. . . . . . 7
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β (πΉ β (Fmlaβsuc π¦) β πΉ β ((Fmlaβπ¦) βͺ {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}))) |
76 | | elun 4148 |
. . . . . . . 8
β’ (πΉ β ((Fmlaβπ¦) βͺ {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}) β (πΉ β (Fmlaβπ¦) β¨ πΉ β {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))})) |
77 | 76 | a1i 11 |
. . . . . . 7
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β (πΉ β ((Fmlaβπ¦) βͺ {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}) β (πΉ β (Fmlaβπ¦) β¨ πΉ β {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}))) |
78 | | simpr 485 |
. . . . . . . . 9
β’ ((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β
(πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) |
79 | 78 | imp 407 |
. . . . . . . 8
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦))) |
80 | 79 | orbi1d 915 |
. . . . . . 7
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β ((πΉ β (Fmlaβπ¦) β¨ πΉ β {π₯ β£ βπ’ β ((β
Sat β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}) β (β¨πΉ, β
β© β ((β
Sat
β
)βπ¦) β¨
πΉ β {π₯ β£ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}))) |
81 | 75, 77, 80 | 3bitrd 304 |
. . . . . 6
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β (πΉ β (Fmlaβsuc π¦) β (β¨πΉ, β
β© β ((β
Sat β
)βπ¦) β¨
πΉ β {π₯ β£ βπ’ β ((β
Sat
β
)βπ¦)(βπ£ β ((β
Sat β
)βπ¦)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}))) |
82 | 66, 72, 81 | 3bitr4rd 311 |
. . . . 5
β’ (((π¦ β Ο β§ (πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦)))) β§
πΉ β V) β (πΉ β (Fmlaβsuc π¦) β β¨πΉ, β
β© β ((β
Sat
β
)βsuc π¦))) |
83 | 82 | exp31 420 |
. . . 4
β’ (π¦ β Ο β ((πΉ β V β (πΉ β (Fmlaβπ¦) β β¨πΉ, β
β© β ((β
Sat
β
)βπ¦))) β
(πΉ β V β (πΉ β (Fmlaβsuc π¦) β β¨πΉ, β
β© β ((β
Sat
β
)βsuc π¦))))) |
84 | 6, 12, 18, 24, 48, 83 | finds 7891 |
. . 3
β’ (π β Ο β (πΉ β V β (πΉ β (Fmlaβπ) β β¨πΉ, β
β© β ((β
Sat
β
)βπ)))) |
85 | 84 | com12 32 |
. 2
β’ (πΉ β V β (π β Ο β (πΉ β (Fmlaβπ) β β¨πΉ, β
β© β ((β
Sat
β
)βπ)))) |
86 | | prcnel 3497 |
. . . . 5
β’ (Β¬
πΉ β V β Β¬
πΉ β (Fmlaβπ)) |
87 | 86 | adantr 481 |
. . . 4
β’ ((Β¬
πΉ β V β§ π β Ο) β Β¬
πΉ β (Fmlaβπ)) |
88 | | opprc1 4897 |
. . . . . 6
β’ (Β¬
πΉ β V β
β¨πΉ, β
β© =
β
) |
89 | 88 | adantr 481 |
. . . . 5
β’ ((Β¬
πΉ β V β§ π β Ο) β
β¨πΉ, β
β© =
β
) |
90 | | satf0n0 34438 |
. . . . . . 7
β’ (π β Ο β β
β ((β
Sat β
)βπ)) |
91 | | df-nel 3047 |
. . . . . . 7
β’ (β
β ((β
Sat β
)βπ) β Β¬ β
β ((β
Sat
β
)βπ)) |
92 | 90, 91 | sylib 217 |
. . . . . 6
β’ (π β Ο β Β¬
β
β ((β
Sat β
)βπ)) |
93 | 92 | adantl 482 |
. . . . 5
β’ ((Β¬
πΉ β V β§ π β Ο) β Β¬
β
β ((β
Sat β
)βπ)) |
94 | 89, 93 | eqneltrd 2853 |
. . . 4
β’ ((Β¬
πΉ β V β§ π β Ο) β Β¬
β¨πΉ, β
β©
β ((β
Sat β
)βπ)) |
95 | 87, 94 | 2falsed 376 |
. . 3
β’ ((Β¬
πΉ β V β§ π β Ο) β (πΉ β (Fmlaβπ) β β¨πΉ, β
β© β ((β
Sat
β
)βπ))) |
96 | 95 | ex 413 |
. 2
β’ (Β¬
πΉ β V β (π β Ο β (πΉ β (Fmlaβπ) β β¨πΉ, β
β© β ((β
Sat
β
)βπ)))) |
97 | 85, 96 | pm2.61i 182 |
1
β’ (π β Ο β (πΉ β (Fmlaβπ) β β¨πΉ, β
β© β ((β
Sat
β
)βπ))) |