Step | Hyp | Ref
| Expression |
1 | | sategoelfvb.s |
. . . . 5
β’ πΈ = (π Satβ (π΄βππ΅)) |
2 | | ovexd 7440 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄βππ΅) β V) |
3 | | simpl 483 |
. . . . . . . . 9
β’ ((π΄ β Ο β§ π΅ β Ο) β π΄ β
Ο) |
4 | | opeq1 4872 |
. . . . . . . . . . . . 13
β’ (π = π΄ β β¨π, πβ© = β¨π΄, πβ©) |
5 | 4 | opeq2d 4879 |
. . . . . . . . . . . 12
β’ (π = π΄ β β¨β
, β¨π, πβ©β© = β¨β
, β¨π΄, πβ©β©) |
6 | 5 | eqeq2d 2743 |
. . . . . . . . . . 11
β’ (π = π΄ β (β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π, πβ©β© β β¨β
,
β¨π΄, π΅β©β© = β¨β
, β¨π΄, πβ©β©)) |
7 | 6 | rexbidv 3178 |
. . . . . . . . . 10
β’ (π = π΄ β (βπ β Ο β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π, πβ©β© β βπ β Ο β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π΄, πβ©β©)) |
8 | 7 | adantl 482 |
. . . . . . . . 9
β’ (((π΄ β Ο β§ π΅ β Ο) β§ π = π΄) β (βπ β Ο β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π, πβ©β© β βπ β Ο β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π΄, πβ©β©)) |
9 | | simpr 485 |
. . . . . . . . . 10
β’ ((π΄ β Ο β§ π΅ β Ο) β π΅ β
Ο) |
10 | | opeq2 4873 |
. . . . . . . . . . . . 13
β’ (π = π΅ β β¨π΄, πβ© = β¨π΄, π΅β©) |
11 | 10 | opeq2d 4879 |
. . . . . . . . . . . 12
β’ (π = π΅ β β¨β
, β¨π΄, πβ©β© = β¨β
, β¨π΄, π΅β©β©) |
12 | 11 | eqeq2d 2743 |
. . . . . . . . . . 11
β’ (π = π΅ β (β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π΄, πβ©β© β β¨β
,
β¨π΄, π΅β©β© = β¨β
, β¨π΄, π΅β©β©)) |
13 | 12 | adantl 482 |
. . . . . . . . . 10
β’ (((π΄ β Ο β§ π΅ β Ο) β§ π = π΅) β (β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π΄, πβ©β© β β¨β
,
β¨π΄, π΅β©β© = β¨β
, β¨π΄, π΅β©β©)) |
14 | | eqidd 2733 |
. . . . . . . . . 10
β’ ((π΄ β Ο β§ π΅ β Ο) β
β¨β
, β¨π΄,
π΅β©β© =
β¨β
, β¨π΄,
π΅β©β©) |
15 | 9, 13, 14 | rspcedvd 3614 |
. . . . . . . . 9
β’ ((π΄ β Ο β§ π΅ β Ο) β
βπ β Ο
β¨β
, β¨π΄,
π΅β©β© =
β¨β
, β¨π΄,
πβ©β©) |
16 | 3, 8, 15 | rspcedvd 3614 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π΅ β Ο) β
βπ β Ο
βπ β Ο
β¨β
, β¨π΄,
π΅β©β© =
β¨β
, β¨π,
πβ©β©) |
17 | | goel 34326 |
. . . . . . . . . 10
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄βππ΅) = β¨β
, β¨π΄, π΅β©β©) |
18 | | goel 34326 |
. . . . . . . . . 10
β’ ((π β Ο β§ π β Ο) β (πβππ) = β¨β
, β¨π, πβ©β©) |
19 | 17, 18 | eqeqan12d 2746 |
. . . . . . . . 9
β’ (((π΄ β Ο β§ π΅ β Ο) β§ (π β Ο β§ π β Ο)) β ((π΄βππ΅) = (πβππ) β β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π, πβ©β©)) |
20 | 19 | 2rexbidva 3217 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π΅ β Ο) β
(βπ β Ο
βπ β Ο
(π΄βππ΅) = (πβππ) β βπ β Ο βπ β Ο β¨β
, β¨π΄, π΅β©β© = β¨β
, β¨π, πβ©β©)) |
21 | 16, 20 | mpbird 256 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β
βπ β Ο
βπ β Ο
(π΄βππ΅) = (πβππ)) |
22 | | eqeq1 2736 |
. . . . . . . . 9
β’ (π₯ = (π΄βππ΅) β (π₯ = (πβππ) β (π΄βππ΅) = (πβππ))) |
23 | 22 | 2rexbidv 3219 |
. . . . . . . 8
β’ (π₯ = (π΄βππ΅) β (βπ β Ο βπ β Ο π₯ = (πβππ) β βπ β Ο βπ β Ο (π΄βππ΅) = (πβππ))) |
24 | | fmla0 34361 |
. . . . . . . 8
β’
(Fmlaββ
) = {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
25 | 23, 24 | elrab2 3685 |
. . . . . . 7
β’ ((π΄βππ΅) β (Fmlaββ
)
β ((π΄βππ΅) β V β§ βπ β Ο βπ β Ο (π΄βππ΅) = (πβππ))) |
26 | 2, 21, 25 | sylanbrc 583 |
. . . . . 6
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄βππ΅) β
(Fmlaββ
)) |
27 | | satefvfmla0 34397 |
. . . . . 6
β’ ((π β π β§ (π΄βππ΅) β (Fmlaββ
)) β (π Satβ (π΄βππ΅)) = {π β (π βm Ο) β£ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd β(2nd
β(π΄βππ΅))))}) |
28 | 26, 27 | sylan2 593 |
. . . . 5
β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β (π Satβ (π΄βππ΅)) = {π β (π βm Ο) β£ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd β(2nd
β(π΄βππ΅))))}) |
29 | 1, 28 | eqtrid 2784 |
. . . 4
β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β πΈ = {π β (π βm Ο) β£ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd β(2nd
β(π΄βππ΅))))}) |
30 | 29 | eleq2d 2819 |
. . 3
β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β (π β πΈ β π β {π β (π βm Ο) β£ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd β(2nd
β(π΄βππ΅))))})) |
31 | | fveq1 6887 |
. . . . 5
β’ (π = π β (πβ(1st β(2nd
β(π΄βππ΅)))) = (πβ(1st
β(2nd β(π΄βππ΅))))) |
32 | | fveq1 6887 |
. . . . 5
β’ (π = π β (πβ(2nd β(2nd
β(π΄βππ΅)))) = (πβ(2nd
β(2nd β(π΄βππ΅))))) |
33 | 31, 32 | eleq12d 2827 |
. . . 4
β’ (π = π β ((πβ(1st β(2nd
β(π΄βππ΅)))) β (πβ(2nd β(2nd
β(π΄βππ΅)))) β (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd
β(2nd β(π΄βππ΅)))))) |
34 | 33 | elrab 3682 |
. . 3
β’ (π β {π β (π βm Ο) β£ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd β(2nd
β(π΄βππ΅))))} β (π β (π βm Ο) β§ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd
β(2nd β(π΄βππ΅)))))) |
35 | 30, 34 | bitrdi 286 |
. 2
β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β (π β πΈ β (π β (π βm Ο) β§ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd
β(2nd β(π΄βππ΅))))))) |
36 | 17 | fveq2d 6892 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π΅ β Ο) β
(2nd β(π΄βππ΅)) = (2nd ββ¨β
,
β¨π΄, π΅β©β©)) |
37 | 36 | fveq2d 6892 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β
(1st β(2nd β(π΄βππ΅))) = (1st β(2nd
ββ¨β
, β¨π΄, π΅β©β©))) |
38 | | 0ex 5306 |
. . . . . . . . . 10
β’ β
β V |
39 | | opex 5463 |
. . . . . . . . . 10
β’
β¨π΄, π΅β© β V |
40 | 38, 39 | op2nd 7980 |
. . . . . . . . 9
β’
(2nd ββ¨β
, β¨π΄, π΅β©β©) = β¨π΄, π΅β© |
41 | 40 | fveq2i 6891 |
. . . . . . . 8
β’
(1st β(2nd ββ¨β
, β¨π΄, π΅β©β©)) = (1st
ββ¨π΄, π΅β©) |
42 | | op1stg 7983 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π΅ β Ο) β
(1st ββ¨π΄, π΅β©) = π΄) |
43 | 41, 42 | eqtrid 2784 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β
(1st β(2nd ββ¨β
, β¨π΄, π΅β©β©)) = π΄) |
44 | 37, 43 | eqtrd 2772 |
. . . . . 6
β’ ((π΄ β Ο β§ π΅ β Ο) β
(1st β(2nd β(π΄βππ΅))) = π΄) |
45 | 44 | fveq2d 6892 |
. . . . 5
β’ ((π΄ β Ο β§ π΅ β Ο) β (πβ(1st
β(2nd β(π΄βππ΅)))) = (πβπ΄)) |
46 | 36 | fveq2d 6892 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β
(2nd β(2nd β(π΄βππ΅))) = (2nd β(2nd
ββ¨β
, β¨π΄, π΅β©β©))) |
47 | 40 | fveq2i 6891 |
. . . . . . . 8
β’
(2nd β(2nd ββ¨β
, β¨π΄, π΅β©β©)) = (2nd
ββ¨π΄, π΅β©) |
48 | | op2ndg 7984 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π΅ β Ο) β
(2nd ββ¨π΄, π΅β©) = π΅) |
49 | 47, 48 | eqtrid 2784 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β
(2nd β(2nd ββ¨β
, β¨π΄, π΅β©β©)) = π΅) |
50 | 46, 49 | eqtrd 2772 |
. . . . . 6
β’ ((π΄ β Ο β§ π΅ β Ο) β
(2nd β(2nd β(π΄βππ΅))) = π΅) |
51 | 50 | fveq2d 6892 |
. . . . 5
β’ ((π΄ β Ο β§ π΅ β Ο) β (πβ(2nd
β(2nd β(π΄βππ΅)))) = (πβπ΅)) |
52 | 45, 51 | eleq12d 2827 |
. . . 4
β’ ((π΄ β Ο β§ π΅ β Ο) β ((πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd
β(2nd β(π΄βππ΅)))) β (πβπ΄) β (πβπ΅))) |
53 | 52 | adantl 482 |
. . 3
β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β ((πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd
β(2nd β(π΄βππ΅)))) β (πβπ΄) β (πβπ΅))) |
54 | 53 | anbi2d 629 |
. 2
β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β ((π β (π βm Ο) β§ (πβ(1st
β(2nd β(π΄βππ΅)))) β (πβ(2nd
β(2nd β(π΄βππ΅))))) β (π β (π βm Ο) β§ (πβπ΄) β (πβπ΅)))) |
55 | 35, 54 | bitrd 278 |
1
β’ ((π β π β§ (π΄ β Ο β§ π΅ β Ο)) β (π β πΈ β (π β (π βm Ο) β§ (πβπ΄) β (πβπ΅)))) |