Step | Hyp | Ref
| Expression |
1 | | oveq1 7415 |
. . . . 5
β’ (π = π΄ β (ππΌπ) = (π΄πΌπ)) |
2 | 1 | eleq2d 2819 |
. . . 4
β’ (π = π΄ β (π β (ππΌπ) β π β (π΄πΌπ))) |
3 | 2 | anbi1d 630 |
. . 3
β’ (π = π΄ β ((π β (ππΌπ) β§ π¦ β (π₯πΌπ§)) β (π β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)))) |
4 | | oveq1 7415 |
. . . . 5
β’ (π = π΄ β (π β π) = (π΄ β π)) |
5 | 4 | eqeq1d 2734 |
. . . 4
β’ (π = π΄ β ((π β π) = (π₯ β π¦) β (π΄ β π) = (π₯ β π¦))) |
6 | 5 | anbi1d 630 |
. . 3
β’ (π = π΄ β (((π β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)) β ((π΄ β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)))) |
7 | | oveq1 7415 |
. . . . 5
β’ (π = π΄ β (π β π) = (π΄ β π)) |
8 | 7 | eqeq1d 2734 |
. . . 4
β’ (π = π΄ β ((π β π) = (π₯ β π€) β (π΄ β π) = (π₯ β π€))) |
9 | 8 | anbi1d 630 |
. . 3
β’ (π = π΄ β (((π β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€)) β ((π΄ β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€)))) |
10 | 3, 6, 9 | 3anbi123d 1436 |
. 2
β’ (π = π΄ β (((π β (ππΌπ) β§ π¦ β (π₯πΌπ§)) β§ ((π β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)) β§ ((π β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€))) β ((π β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)) β§ ((π΄ β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€))))) |
11 | | eleq1 2821 |
. . . 4
β’ (π = π΅ β (π β (π΄πΌπ) β π΅ β (π΄πΌπ))) |
12 | 11 | anbi1d 630 |
. . 3
β’ (π = π΅ β ((π β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)) β (π΅ β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)))) |
13 | | oveq2 7416 |
. . . . 5
β’ (π = π΅ β (π΄ β π) = (π΄ β π΅)) |
14 | 13 | eqeq1d 2734 |
. . . 4
β’ (π = π΅ β ((π΄ β π) = (π₯ β π¦) β (π΄ β π΅) = (π₯ β π¦))) |
15 | | oveq1 7415 |
. . . . 5
β’ (π = π΅ β (π β π) = (π΅ β π)) |
16 | 15 | eqeq1d 2734 |
. . . 4
β’ (π = π΅ β ((π β π) = (π¦ β π§) β (π΅ β π) = (π¦ β π§))) |
17 | 14, 16 | anbi12d 631 |
. . 3
β’ (π = π΅ β (((π΄ β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)) β ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β π) = (π¦ β π§)))) |
18 | | oveq1 7415 |
. . . . 5
β’ (π = π΅ β (π β π) = (π΅ β π)) |
19 | 18 | eqeq1d 2734 |
. . . 4
β’ (π = π΅ β ((π β π) = (π¦ β π€) β (π΅ β π) = (π¦ β π€))) |
20 | 19 | anbi2d 629 |
. . 3
β’ (π = π΅ β (((π΄ β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€)) β ((π΄ β π) = (π₯ β π€) β§ (π΅ β π) = (π¦ β π€)))) |
21 | 12, 17, 20 | 3anbi123d 1436 |
. 2
β’ (π = π΅ β (((π β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)) β§ ((π΄ β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€))) β ((π΅ β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β π) = (π¦ β π§)) β§ ((π΄ β π) = (π₯ β π€) β§ (π΅ β π) = (π¦ β π€))))) |
22 | | oveq2 7416 |
. . . . 5
β’ (π = πΆ β (π΄πΌπ) = (π΄πΌπΆ)) |
23 | 22 | eleq2d 2819 |
. . . 4
β’ (π = πΆ β (π΅ β (π΄πΌπ) β π΅ β (π΄πΌπΆ))) |
24 | 23 | anbi1d 630 |
. . 3
β’ (π = πΆ β ((π΅ β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)) β (π΅ β (π΄πΌπΆ) β§ π¦ β (π₯πΌπ§)))) |
25 | | oveq2 7416 |
. . . . 5
β’ (π = πΆ β (π΅ β π) = (π΅ β πΆ)) |
26 | 25 | eqeq1d 2734 |
. . . 4
β’ (π = πΆ β ((π΅ β π) = (π¦ β π§) β (π΅ β πΆ) = (π¦ β π§))) |
27 | 26 | anbi2d 629 |
. . 3
β’ (π = πΆ β (((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β π) = (π¦ β π§)) β ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β πΆ) = (π¦ β π§)))) |
28 | 24, 27 | 3anbi12d 1437 |
. 2
β’ (π = πΆ β (((π΅ β (π΄πΌπ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β π) = (π¦ β π§)) β§ ((π΄ β π) = (π₯ β π€) β§ (π΅ β π) = (π¦ β π€))) β ((π΅ β (π΄πΌπΆ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β§ ((π΄ β π) = (π₯ β π€) β§ (π΅ β π) = (π¦ β π€))))) |
29 | | oveq2 7416 |
. . . . 5
β’ (π = π· β (π΄ β π) = (π΄ β π·)) |
30 | 29 | eqeq1d 2734 |
. . . 4
β’ (π = π· β ((π΄ β π) = (π₯ β π€) β (π΄ β π·) = (π₯ β π€))) |
31 | | oveq2 7416 |
. . . . 5
β’ (π = π· β (π΅ β π) = (π΅ β π·)) |
32 | 31 | eqeq1d 2734 |
. . . 4
β’ (π = π· β ((π΅ β π) = (π¦ β π€) β (π΅ β π·) = (π¦ β π€))) |
33 | 30, 32 | anbi12d 631 |
. . 3
β’ (π = π· β (((π΄ β π) = (π₯ β π€) β§ (π΅ β π) = (π¦ β π€)) β ((π΄ β π·) = (π₯ β π€) β§ (π΅ β π·) = (π¦ β π€)))) |
34 | 33 | 3anbi3d 1442 |
. 2
β’ (π = π· β (((π΅ β (π΄πΌπΆ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β§ ((π΄ β π) = (π₯ β π€) β§ (π΅ β π) = (π¦ β π€))) β ((π΅ β (π΄πΌπΆ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β§ ((π΄ β π·) = (π₯ β π€) β§ (π΅ β π·) = (π¦ β π€))))) |
35 | | oveq1 7415 |
. . . . 5
β’ (π₯ = π β (π₯πΌπ§) = (ππΌπ§)) |
36 | 35 | eleq2d 2819 |
. . . 4
β’ (π₯ = π β (π¦ β (π₯πΌπ§) β π¦ β (ππΌπ§))) |
37 | 36 | anbi2d 629 |
. . 3
β’ (π₯ = π β ((π΅ β (π΄πΌπΆ) β§ π¦ β (π₯πΌπ§)) β (π΅ β (π΄πΌπΆ) β§ π¦ β (ππΌπ§)))) |
38 | | oveq1 7415 |
. . . . 5
β’ (π₯ = π β (π₯ β π¦) = (π β π¦)) |
39 | 38 | eqeq2d 2743 |
. . . 4
β’ (π₯ = π β ((π΄ β π΅) = (π₯ β π¦) β (π΄ β π΅) = (π β π¦))) |
40 | 39 | anbi1d 630 |
. . 3
β’ (π₯ = π β (((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β ((π΄ β π΅) = (π β π¦) β§ (π΅ β πΆ) = (π¦ β π§)))) |
41 | | oveq1 7415 |
. . . . 5
β’ (π₯ = π β (π₯ β π€) = (π β π€)) |
42 | 41 | eqeq2d 2743 |
. . . 4
β’ (π₯ = π β ((π΄ β π·) = (π₯ β π€) β (π΄ β π·) = (π β π€))) |
43 | 42 | anbi1d 630 |
. . 3
β’ (π₯ = π β (((π΄ β π·) = (π₯ β π€) β§ (π΅ β π·) = (π¦ β π€)) β ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π¦ β π€)))) |
44 | 37, 40, 43 | 3anbi123d 1436 |
. 2
β’ (π₯ = π β (((π΅ β (π΄πΌπΆ) β§ π¦ β (π₯πΌπ§)) β§ ((π΄ β π΅) = (π₯ β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β§ ((π΄ β π·) = (π₯ β π€) β§ (π΅ β π·) = (π¦ β π€))) β ((π΅ β (π΄πΌπΆ) β§ π¦ β (ππΌπ§)) β§ ((π΄ β π΅) = (π β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β§ ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π¦ β π€))))) |
45 | | eleq1 2821 |
. . . 4
β’ (π¦ = π β (π¦ β (ππΌπ§) β π β (ππΌπ§))) |
46 | 45 | anbi2d 629 |
. . 3
β’ (π¦ = π β ((π΅ β (π΄πΌπΆ) β§ π¦ β (ππΌπ§)) β (π΅ β (π΄πΌπΆ) β§ π β (ππΌπ§)))) |
47 | | oveq2 7416 |
. . . . 5
β’ (π¦ = π β (π β π¦) = (π β π)) |
48 | 47 | eqeq2d 2743 |
. . . 4
β’ (π¦ = π β ((π΄ β π΅) = (π β π¦) β (π΄ β π΅) = (π β π))) |
49 | | oveq1 7415 |
. . . . 5
β’ (π¦ = π β (π¦ β π§) = (π β π§)) |
50 | 49 | eqeq2d 2743 |
. . . 4
β’ (π¦ = π β ((π΅ β πΆ) = (π¦ β π§) β (π΅ β πΆ) = (π β π§))) |
51 | 48, 50 | anbi12d 631 |
. . 3
β’ (π¦ = π β (((π΄ β π΅) = (π β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π§)))) |
52 | | oveq1 7415 |
. . . . 5
β’ (π¦ = π β (π¦ β π€) = (π β π€)) |
53 | 52 | eqeq2d 2743 |
. . . 4
β’ (π¦ = π β ((π΅ β π·) = (π¦ β π€) β (π΅ β π·) = (π β π€))) |
54 | 53 | anbi2d 629 |
. . 3
β’ (π¦ = π β (((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π¦ β π€)) β ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π β π€)))) |
55 | 46, 51, 54 | 3anbi123d 1436 |
. 2
β’ (π¦ = π β (((π΅ β (π΄πΌπΆ) β§ π¦ β (ππΌπ§)) β§ ((π΄ β π΅) = (π β π¦) β§ (π΅ β πΆ) = (π¦ β π§)) β§ ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π¦ β π€))) β ((π΅ β (π΄πΌπΆ) β§ π β (ππΌπ§)) β§ ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π§)) β§ ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π β π€))))) |
56 | | oveq2 7416 |
. . . . 5
β’ (π§ = π β (ππΌπ§) = (ππΌπ)) |
57 | 56 | eleq2d 2819 |
. . . 4
β’ (π§ = π β (π β (ππΌπ§) β π β (ππΌπ))) |
58 | 57 | anbi2d 629 |
. . 3
β’ (π§ = π β ((π΅ β (π΄πΌπΆ) β§ π β (ππΌπ§)) β (π΅ β (π΄πΌπΆ) β§ π β (ππΌπ)))) |
59 | | oveq2 7416 |
. . . . 5
β’ (π§ = π β (π β π§) = (π β π)) |
60 | 59 | eqeq2d 2743 |
. . . 4
β’ (π§ = π β ((π΅ β πΆ) = (π β π§) β (π΅ β πΆ) = (π β π))) |
61 | 60 | anbi2d 629 |
. . 3
β’ (π§ = π β (((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π§)) β ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π)))) |
62 | 58, 61 | 3anbi12d 1437 |
. 2
β’ (π§ = π β (((π΅ β (π΄πΌπΆ) β§ π β (ππΌπ§)) β§ ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π§)) β§ ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π β π€))) β ((π΅ β (π΄πΌπΆ) β§ π β (ππΌπ)) β§ ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π)) β§ ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π β π€))))) |
63 | | oveq2 7416 |
. . . . 5
β’ (π€ = π β (π β π€) = (π β π)) |
64 | 63 | eqeq2d 2743 |
. . . 4
β’ (π€ = π β ((π΄ β π·) = (π β π€) β (π΄ β π·) = (π β π))) |
65 | | oveq2 7416 |
. . . . 5
β’ (π€ = π β (π β π€) = (π β π)) |
66 | 65 | eqeq2d 2743 |
. . . 4
β’ (π€ = π β ((π΅ β π·) = (π β π€) β (π΅ β π·) = (π β π))) |
67 | 64, 66 | anbi12d 631 |
. . 3
β’ (π€ = π β (((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π β π€)) β ((π΄ β π·) = (π β π) β§ (π΅ β π·) = (π β π)))) |
68 | 67 | 3anbi3d 1442 |
. 2
β’ (π€ = π β (((π΅ β (π΄πΌπΆ) β§ π β (ππΌπ)) β§ ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π)) β§ ((π΄ β π·) = (π β π€) β§ (π΅ β π·) = (π β π€))) β ((π΅ β (π΄πΌπΆ) β§ π β (ππΌπ)) β§ ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π)) β§ ((π΄ β π·) = (π β π) β§ (π΅ β π·) = (π β π))))) |
69 | | brafs.o |
. . 3
β’ π = (AFSβπΊ) |
70 | | brafs.p |
. . . 4
β’ π = (BaseβπΊ) |
71 | | brafs.d |
. . . 4
β’ β =
(distβπΊ) |
72 | | brafs.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
73 | | brafs.g |
. . . 4
β’ (π β πΊ β TarskiG) |
74 | 70, 71, 72, 73 | afsval 33678 |
. . 3
β’ (π β (AFSβπΊ) = {β¨π, πβ© β£ βπ β π βπ β π βπ β π βπ β π βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π₯, π¦β©, β¨π§, π€β©β© β§ ((π β (ππΌπ) β§ π¦ β (π₯πΌπ§)) β§ ((π β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)) β§ ((π β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€))))}) |
75 | 69, 74 | eqtrid 2784 |
. 2
β’ (π β π = {β¨π, πβ© β£ βπ β π βπ β π βπ β π βπ β π βπ₯ β π βπ¦ β π βπ§ β π βπ€ β π (π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π₯, π¦β©, β¨π§, π€β©β© β§ ((π β (ππΌπ) β§ π¦ β (π₯πΌπ§)) β§ ((π β π) = (π₯ β π¦) β§ (π β π) = (π¦ β π§)) β§ ((π β π) = (π₯ β π€) β§ (π β π) = (π¦ β π€))))}) |
76 | | brafs.1 |
. 2
β’ (π β π΄ β π) |
77 | | brafs.2 |
. 2
β’ (π β π΅ β π) |
78 | | brafs.3 |
. 2
β’ (π β πΆ β π) |
79 | | brafs.4 |
. 2
β’ (π β π· β π) |
80 | | brafs.5 |
. 2
β’ (π β π β π) |
81 | | brafs.6 |
. 2
β’ (π β π β π) |
82 | | brafs.7 |
. 2
β’ (π β π β π) |
83 | | brafs.8 |
. 2
β’ (π β π β π) |
84 | 10, 21, 28, 34, 44, 55, 62, 68, 75, 76, 77, 78, 79, 80, 81, 82, 83 | br8d 31834 |
1
β’ (π β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©πβ¨β¨π, πβ©, β¨π, πβ©β© β ((π΅ β (π΄πΌπΆ) β§ π β (ππΌπ)) β§ ((π΄ β π΅) = (π β π) β§ (π΅ β πΆ) = (π β π)) β§ ((π΄ β π·) = (π β π) β§ (π΅ β π·) = (π β π))))) |