Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . . 6
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β πΌ β
Ο) |
2 | | simplr 768 |
. . . . . 6
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β π½ β
Ο) |
3 | | simprl 770 |
. . . . . 6
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β πΎ β
Ο) |
4 | | simprr 772 |
. . . . . . . 8
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β πΏ β
Ο) |
5 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π = πΏ β (πΎβππ) = (πΎβππΏ)) |
6 | 5 | oveq2d 7425 |
. . . . . . . . . 10
β’ (π = πΏ β ((πΌβππ½)βΌπ(πΎβππ)) = ((πΌβππ½)βΌπ(πΎβππΏ))) |
7 | 6 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = πΏ β (π = ((πΌβππ½)βΌπ(πΎβππ)) β π = ((πΌβππ½)βΌπ(πΎβππΏ)))) |
8 | 7 | adantl 483 |
. . . . . . . 8
β’ ((((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β§ π = πΏ) β (π = ((πΌβππ½)βΌπ(πΎβππ)) β π = ((πΌβππ½)βΌπ(πΎβππΏ)))) |
9 | | satfv1fvfmla1.x |
. . . . . . . . 9
β’ π = ((πΌβππ½)βΌπ(πΎβππΏ)) |
10 | 9 | a1i 11 |
. . . . . . . 8
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β π = ((πΌβππ½)βΌπ(πΎβππΏ))) |
11 | 4, 8, 10 | rspcedvd 3615 |
. . . . . . 7
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β
βπ β Ο
π = ((πΌβππ½)βΌπ(πΎβππ))) |
12 | 11 | orcd 872 |
. . . . . 6
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β
(βπ β Ο
π = ((πΌβππ½)βΌπ(πΎβππ)) β¨ π = βππΎ(πΌβππ½))) |
13 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π = πΌ β (πβππ) = (πΌβππ)) |
14 | 13 | oveq1d 7424 |
. . . . . . . . . 10
β’ (π = πΌ β ((πβππ)βΌπ(πβππ)) = ((πΌβππ)βΌπ(πβππ))) |
15 | 14 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = πΌ β (π = ((πβππ)βΌπ(πβππ)) β π = ((πΌβππ)βΌπ(πβππ)))) |
16 | 15 | rexbidv 3179 |
. . . . . . . 8
β’ (π = πΌ β (βπ β Ο π = ((πβππ)βΌπ(πβππ)) β βπ β Ο π = ((πΌβππ)βΌπ(πβππ)))) |
17 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π = πΌ β π = π) |
18 | 17, 13 | goaleq12d 34342 |
. . . . . . . . 9
β’ (π = πΌ β βππ(πβππ) = βππ(πΌβππ)) |
19 | 18 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = πΌ β (π = βππ(πβππ) β π = βππ(πΌβππ))) |
20 | 16, 19 | orbi12d 918 |
. . . . . . 7
β’ (π = πΌ β ((βπ β Ο π = ((πβππ)βΌπ(πβππ)) β¨ π = βππ(πβππ)) β (βπ β Ο π = ((πΌβππ)βΌπ(πβππ)) β¨ π = βππ(πΌβππ)))) |
21 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π = π½ β (πΌβππ) = (πΌβππ½)) |
22 | 21 | oveq1d 7424 |
. . . . . . . . . 10
β’ (π = π½ β ((πΌβππ)βΌπ(πβππ)) = ((πΌβππ½)βΌπ(πβππ))) |
23 | 22 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = π½ β (π = ((πΌβππ)βΌπ(πβππ)) β π = ((πΌβππ½)βΌπ(πβππ)))) |
24 | 23 | rexbidv 3179 |
. . . . . . . 8
β’ (π = π½ β (βπ β Ο π = ((πΌβππ)βΌπ(πβππ)) β βπ β Ο π = ((πΌβππ½)βΌπ(πβππ)))) |
25 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π = π½ β π = π) |
26 | 25, 21 | goaleq12d 34342 |
. . . . . . . . 9
β’ (π = π½ β βππ(πΌβππ) = βππ(πΌβππ½)) |
27 | 26 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = π½ β (π = βππ(πΌβππ) β π = βππ(πΌβππ½))) |
28 | 24, 27 | orbi12d 918 |
. . . . . . 7
β’ (π = π½ β ((βπ β Ο π = ((πΌβππ)βΌπ(πβππ)) β¨ π = βππ(πΌβππ)) β (βπ β Ο π = ((πΌβππ½)βΌπ(πβππ)) β¨ π = βππ(πΌβππ½)))) |
29 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π = πΎ β (πβππ) = (πΎβππ)) |
30 | 29 | oveq2d 7425 |
. . . . . . . . . 10
β’ (π = πΎ β ((πΌβππ½)βΌπ(πβππ)) = ((πΌβππ½)βΌπ(πΎβππ))) |
31 | 30 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = πΎ β (π = ((πΌβππ½)βΌπ(πβππ)) β π = ((πΌβππ½)βΌπ(πΎβππ)))) |
32 | 31 | rexbidv 3179 |
. . . . . . . 8
β’ (π = πΎ β (βπ β Ο π = ((πΌβππ½)βΌπ(πβππ)) β βπ β Ο π = ((πΌβππ½)βΌπ(πΎβππ)))) |
33 | | id 22 |
. . . . . . . . . 10
β’ (π = πΎ β π = πΎ) |
34 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π = πΎ β (πΌβππ½) = (πΌβππ½)) |
35 | 33, 34 | goaleq12d 34342 |
. . . . . . . . 9
β’ (π = πΎ β βππ(πΌβππ½) = βππΎ(πΌβππ½)) |
36 | 35 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = πΎ β (π = βππ(πΌβππ½) β π = βππΎ(πΌβππ½))) |
37 | 32, 36 | orbi12d 918 |
. . . . . . 7
β’ (π = πΎ β ((βπ β Ο π = ((πΌβππ½)βΌπ(πβππ)) β¨ π = βππ(πΌβππ½)) β (βπ β Ο π = ((πΌβππ½)βΌπ(πΎβππ)) β¨ π = βππΎ(πΌβππ½)))) |
38 | 20, 28, 37 | rspc3ev 3629 |
. . . . . 6
β’ (((πΌ β Ο β§ π½ β Ο β§ πΎ β Ο) β§
(βπ β Ο
π = ((πΌβππ½)βΌπ(πΎβππ)) β¨ π = βππΎ(πΌβππ½))) β βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π = ((πβππ)βΌπ(πβππ)) β¨ π = βππ(πβππ))) |
39 | 1, 2, 3, 12, 38 | syl31anc 1374 |
. . . . 5
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β
βπ β Ο
βπ β Ο
βπ β Ο
(βπ β Ο
π = ((πβππ)βΌπ(πβππ)) β¨ π = βππ(πβππ))) |
40 | 9 | ovexi 7443 |
. . . . . 6
β’ π β V |
41 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ = ((πβππ)βΌπ(πβππ)) β π = ((πβππ)βΌπ(πβππ)))) |
42 | 41 | rexbidv 3179 |
. . . . . . . . 9
β’ (π₯ = π β (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β βπ β Ο π = ((πβππ)βΌπ(πβππ)))) |
43 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ = βππ(πβππ) β π = βππ(πβππ))) |
44 | 42, 43 | orbi12d 918 |
. . . . . . . 8
β’ (π₯ = π β ((βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ)) β (βπ β Ο π = ((πβππ)βΌπ(πβππ)) β¨ π = βππ(πβππ)))) |
45 | 44 | rexbidv 3179 |
. . . . . . 7
β’ (π₯ = π β (βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ)) β βπ β Ο (βπ β Ο π = ((πβππ)βΌπ(πβππ)) β¨ π = βππ(πβππ)))) |
46 | 45 | 2rexbidv 3220 |
. . . . . 6
β’ (π₯ = π β (βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ)) β βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π = ((πβππ)βΌπ(πβππ)) β¨ π = βππ(πβππ)))) |
47 | 40, 46 | elab 3669 |
. . . . 5
β’ (π β {π₯ β£ βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))} β βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π = ((πβππ)βΌπ(πβππ)) β¨ π = βππ(πβππ))) |
48 | 39, 47 | sylibr 233 |
. . . 4
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β π β {π₯ β£ βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))}) |
49 | 48 | olcd 873 |
. . 3
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β (π β ({β
} Γ
(Ο Γ Ο)) β¨ π β {π₯ β£ βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))})) |
50 | | elun 4149 |
. . 3
β’ (π β (({β
} Γ
(Ο Γ Ο)) βͺ {π₯ β£ βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))}) β (π β ({β
} Γ (Ο Γ
Ο)) β¨ π β
{π₯ β£ βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))})) |
51 | 49, 50 | sylibr 233 |
. 2
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β π β (({β
} Γ
(Ο Γ Ο)) βͺ {π₯ β£ βπ β Ο βπ β Ο βπ β Ο (βπ β Ο π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))})) |
52 | | fmla1 34378 |
. 2
β’
(Fmlaβ1o) = (({β
} Γ (Ο Γ
Ο)) βͺ {π₯ β£
βπ β Ο
βπ β Ο
βπ β Ο
(βπ β Ο
π₯ = ((πβππ)βΌπ(πβππ)) β¨ π₯ = βππ(πβππ))}) |
53 | 51, 52 | eleqtrrdi 2845 |
1
β’ (((πΌ β Ο β§ π½ β Ο) β§ (πΎ β Ο β§ πΏ β Ο)) β π β
(Fmlaβ1o)) |