Step | Hyp | Ref
| Expression |
1 | | ssid 3967 |
. 2
β’ π΄ β π΄ |
2 | | aomclem6.a |
. . . 4
β’ (π β π΄ β On) |
3 | 2 | adantr 482 |
. . 3
β’ ((π β§ π΄ β π΄) β π΄ β On) |
4 | | sseq1 3970 |
. . . . . 6
β’ (π = π β (π β π΄ β π β π΄)) |
5 | 4 | anbi2d 630 |
. . . . 5
β’ (π = π β ((π β§ π β π΄) β (π β§ π β π΄))) |
6 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (π»βπ) = (π»βπ)) |
7 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (π
1βπ) =
(π
1βπ)) |
8 | 6, 7 | weeq12d 41370 |
. . . . 5
β’ (π = π β ((π»βπ) We (π
1βπ) β (π»βπ) We (π
1βπ))) |
9 | 5, 8 | imbi12d 345 |
. . . 4
β’ (π = π β (((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β ((π β§ π β π΄) β (π»βπ) We (π
1βπ)))) |
10 | | sseq1 3970 |
. . . . . 6
β’ (π = π΄ β (π β π΄ β π΄ β π΄)) |
11 | 10 | anbi2d 630 |
. . . . 5
β’ (π = π΄ β ((π β§ π β π΄) β (π β§ π΄ β π΄))) |
12 | | fveq2 6843 |
. . . . . 6
β’ (π = π΄ β (π»βπ) = (π»βπ΄)) |
13 | | fveq2 6843 |
. . . . . 6
β’ (π = π΄ β (π
1βπ) =
(π
1βπ΄)) |
14 | 12, 13 | weeq12d 41370 |
. . . . 5
β’ (π = π΄ β ((π»βπ) We (π
1βπ) β (π»βπ΄) We (π
1βπ΄))) |
15 | 11, 14 | imbi12d 345 |
. . . 4
β’ (π = π΄ β (((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β ((π β§ π΄ β π΄) β (π»βπ΄) We (π
1βπ΄)))) |
16 | | aomclem6.b |
. . . . . . . . . . . . . 14
β’ π΅ = {β¨π, πβ© β£ βπ β (π
1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} |
17 | | aomclem6.c |
. . . . . . . . . . . . . 14
β’ πΆ = (π β V β¦ sup((π¦βπ), (π
1βdom π§), π΅)) |
18 | | aomclem6.d |
. . . . . . . . . . . . . 14
β’ π· = recs((π β V β¦ (πΆβ((π
1βdom
π§) β ran π)))) |
19 | | aomclem6.e |
. . . . . . . . . . . . . 14
β’ πΈ = {β¨π, πβ© β£ β©
(β‘π· β {π}) β β© (β‘π· β {π})} |
20 | | aomclem6.f |
. . . . . . . . . . . . . 14
β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} |
21 | | aomclem6.g |
. . . . . . . . . . . . . 14
β’ πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) |
22 | | dmeq 5860 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π» βΎ π) β dom π§ = dom (π» βΎ π)) |
23 | 22 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β dom π§ = dom (π» βΎ π)) |
24 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β π β On) |
25 | | onss 7720 |
. . . . . . . . . . . . . . . . 17
β’ (π β On β π β On) |
26 | | aomclem6.h |
. . . . . . . . . . . . . . . . . . 19
β’ π» = recs((π§ β V β¦ πΊ)) |
27 | 26 | tfr1 8344 |
. . . . . . . . . . . . . . . . . 18
β’ π» Fn On |
28 | | fnssres 6625 |
. . . . . . . . . . . . . . . . . 18
β’ ((π» Fn On β§ π β On) β (π» βΎ π) Fn π) |
29 | 27, 28 | mpan 689 |
. . . . . . . . . . . . . . . . 17
β’ (π β On β (π» βΎ π) Fn π) |
30 | | fndm 6606 |
. . . . . . . . . . . . . . . . 17
β’ ((π» βΎ π) Fn π β dom (π» βΎ π) = π) |
31 | 24, 25, 29, 30 | 4syl 19 |
. . . . . . . . . . . . . . . 16
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β dom (π» βΎ π) = π) |
32 | 23, 31 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β dom π§ = π) |
33 | 32, 24 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β dom π§ β On) |
34 | 32 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β (π β dom π§ β π β π)) |
35 | 34 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β π β π) |
36 | | simpll2 1214 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ))) |
37 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β π) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β π) |
39 | | onelss 6360 |
. . . . . . . . . . . . . . . . . . . 20
β’ (dom
π§ β On β (π β dom π§ β π β dom π§)) |
40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β (π β dom π§ β π β dom π§)) |
41 | 40 | imp 408 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β π β dom π§) |
42 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β π β π΄) |
43 | 32, 42 | eqsstrd 3983 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β dom π§ β π΄) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β dom π§ β π΄) |
45 | 41, 44 | sstrd 3955 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β π β π΄) |
46 | | sseq1 3970 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π β π΄ β π β π΄)) |
47 | 46 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((π β§ π β π΄) β (π β§ π β π΄))) |
48 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π»βπ) = (π»βπ)) |
49 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π
1βπ) =
(π
1βπ)) |
50 | 48, 49 | weeq12d 41370 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((π»βπ) We (π
1βπ) β (π»βπ) We (π
1βπ))) |
51 | 47, 50 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β ((π β§ π β π΄) β (π»βπ) We (π
1βπ)))) |
52 | 51 | rspcva 3580 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ))) β ((π β§ π β π΄) β (π»βπ) We (π
1βπ))) |
53 | 52 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ))) β§ (π β§ π β π΄)) β (π»βπ) We (π
1βπ)) |
54 | 35, 36, 38, 45, 53 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β (π»βπ) We (π
1βπ)) |
55 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (π» βΎ π) β (π§βπ) = ((π» βΎ π)βπ)) |
56 | 55 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β (π§βπ) = ((π» βΎ π)βπ)) |
57 | | fvres 6862 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β ((π» βΎ π)βπ) = (π»βπ)) |
58 | 35, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β ((π» βΎ π)βπ) = (π»βπ)) |
59 | 56, 58 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β (π§βπ) = (π»βπ)) |
60 | | weeq1 5622 |
. . . . . . . . . . . . . . . . 17
β’ ((π§βπ) = (π»βπ) β ((π§βπ) We (π
1βπ) β (π»βπ) We (π
1βπ))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β ((π§βπ) We (π
1βπ) β (π»βπ) We (π
1βπ))) |
62 | 54, 61 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β§ π β dom π§) β (π§βπ) We (π
1βπ)) |
63 | 62 | ralrimiva 3144 |
. . . . . . . . . . . . . 14
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β βπ β dom π§(π§βπ) We (π
1βπ)) |
64 | 37, 2 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β π΄ β On) |
65 | | aomclem6.y |
. . . . . . . . . . . . . . 15
β’ (π β βπ β π«
(π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
66 | 37, 65 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β βπ β π«
(π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
67 | 16, 17, 18, 19, 20, 21, 33, 63, 64, 43, 66 | aomclem5 41388 |
. . . . . . . . . . . . 13
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β πΊ We (π
1βdom π§)) |
68 | 32 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β (π
1βdom
π§) =
(π
1βπ)) |
69 | | weeq2 5623 |
. . . . . . . . . . . . . 14
β’
((π
1βdom π§) = (π
1βπ) β (πΊ We (π
1βdom π§) β πΊ We (π
1βπ))) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β (πΊ We (π
1βdom π§) β πΊ We (π
1βπ))) |
71 | 67, 70 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β§ π§ = (π» βΎ π)) β πΊ We (π
1βπ)) |
72 | 71 | ex 414 |
. . . . . . . . . . 11
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β (π§ = (π» βΎ π) β πΊ We (π
1βπ))) |
73 | 72 | alrimiv 1931 |
. . . . . . . . . 10
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β βπ§(π§ = (π» βΎ π) β πΊ We (π
1βπ))) |
74 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π(π§ = (π» βΎ π) β πΊ We (π
1βπ)) |
75 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π§ π = (π» βΎ π) |
76 | | nfsbc1v 3760 |
. . . . . . . . . . . 12
β’
β²π§[π / π§]πΊ We (π
1βπ) |
77 | 75, 76 | nfim 1900 |
. . . . . . . . . . 11
β’
β²π§(π = (π» βΎ π) β [π / π§]πΊ We (π
1βπ)) |
78 | | eqeq1 2741 |
. . . . . . . . . . . 12
β’ (π§ = π β (π§ = (π» βΎ π) β π = (π» βΎ π))) |
79 | | sbceq1a 3751 |
. . . . . . . . . . . 12
β’ (π§ = π β (πΊ We (π
1βπ) β [π / π§]πΊ We (π
1βπ))) |
80 | 78, 79 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π§ = π β ((π§ = (π» βΎ π) β πΊ We (π
1βπ)) β (π = (π» βΎ π) β [π / π§]πΊ We (π
1βπ)))) |
81 | 74, 77, 80 | cbvalv1 2338 |
. . . . . . . . . 10
β’
(βπ§(π§ = (π» βΎ π) β πΊ We (π
1βπ)) β βπ(π = (π» βΎ π) β [π / π§]πΊ We (π
1βπ))) |
82 | 73, 81 | sylib 217 |
. . . . . . . . 9
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β βπ(π = (π» βΎ π) β [π / π§]πΊ We (π
1βπ))) |
83 | | nfsbc1v 3760 |
. . . . . . . . . 10
β’
β²π[(π» βΎ π) / π][π / π§]πΊ We (π
1βπ) |
84 | | fnfun 6603 |
. . . . . . . . . . . 12
β’ (π» Fn On β Fun π») |
85 | 27, 84 | ax-mp 5 |
. . . . . . . . . . 11
β’ Fun π» |
86 | | vex 3450 |
. . . . . . . . . . 11
β’ π β V |
87 | | resfunexg 7166 |
. . . . . . . . . . 11
β’ ((Fun
π» β§ π β V) β (π» βΎ π) β V) |
88 | 85, 86, 87 | mp2an 691 |
. . . . . . . . . 10
β’ (π» βΎ π) β V |
89 | | sbceq1a 3751 |
. . . . . . . . . 10
β’ (π = (π» βΎ π) β ([π / π§]πΊ We (π
1βπ) β [(π» βΎ π) / π][π / π§]πΊ We (π
1βπ))) |
90 | 83, 88, 89 | ceqsal 3480 |
. . . . . . . . 9
β’
(βπ(π = (π» βΎ π) β [π / π§]πΊ We (π
1βπ)) β [(π» βΎ π) / π][π / π§]πΊ We (π
1βπ)) |
91 | 82, 90 | sylib 217 |
. . . . . . . 8
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β [(π» βΎ π) / π][π / π§]πΊ We (π
1βπ)) |
92 | | sbccow 3763 |
. . . . . . . 8
β’
([(π» βΎ
π) / π][π / π§]πΊ We (π
1βπ) β [(π» βΎ π) / π§]πΊ We (π
1βπ)) |
93 | 91, 92 | sylib 217 |
. . . . . . 7
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β [(π» βΎ π) / π§]πΊ We (π
1βπ)) |
94 | | nfcsb1v 3881 |
. . . . . . . . . 10
β’
β²π§β¦(π» βΎ π) / π§β¦πΊ |
95 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π§(π
1βπ) |
96 | 94, 95 | nfwe 5610 |
. . . . . . . . 9
β’
β²π§β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ) |
97 | | csbeq1a 3870 |
. . . . . . . . . 10
β’ (π§ = (π» βΎ π) β πΊ = β¦(π» βΎ π) / π§β¦πΊ) |
98 | | weeq1 5622 |
. . . . . . . . . 10
β’ (πΊ = β¦(π» βΎ π) / π§β¦πΊ β (πΊ We (π
1βπ) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ))) |
99 | 97, 98 | syl 17 |
. . . . . . . . 9
β’ (π§ = (π» βΎ π) β (πΊ We (π
1βπ) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ))) |
100 | 96, 99 | sbciegf 3779 |
. . . . . . . 8
β’ ((π» βΎ π) β V β ([(π» βΎ π) / π§]πΊ We (π
1βπ) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ))) |
101 | 88, 100 | ax-mp 5 |
. . . . . . 7
β’
([(π» βΎ
π) / π§]πΊ We (π
1βπ) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ)) |
102 | 93, 101 | sylib 217 |
. . . . . 6
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ)) |
103 | | recsval 8351 |
. . . . . . . . 9
β’ (π β On β (recs((π§ β V β¦ πΊ))βπ) = ((π§ β V β¦ πΊ)β(recs((π§ β V β¦ πΊ)) βΎ π))) |
104 | 26 | fveq1i 6844 |
. . . . . . . . 9
β’ (π»βπ) = (recs((π§ β V β¦ πΊ))βπ) |
105 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’
(π
1βdom π§) β V |
106 | 105, 105 | xpex 7688 |
. . . . . . . . . . . . . 14
β’
((π
1βdom π§) Γ (π
1βdom
π§)) β
V |
107 | 106 | inex2 5276 |
. . . . . . . . . . . . 13
β’ (if(dom
π§ = βͺ dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) β V |
108 | 21, 107 | eqeltri 2834 |
. . . . . . . . . . . 12
β’ πΊ β V |
109 | 108 | csbex 5269 |
. . . . . . . . . . 11
β’
β¦(π»
βΎ π) / π§β¦πΊ β V |
110 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π§ β V β¦ πΊ) = (π§ β V β¦ πΊ) |
111 | 110 | fvmpts 6952 |
. . . . . . . . . . 11
β’ (((π» βΎ π) β V β§ β¦(π» βΎ π) / π§β¦πΊ β V) β ((π§ β V β¦ πΊ)β(π» βΎ π)) = β¦(π» βΎ π) / π§β¦πΊ) |
112 | 88, 109, 111 | mp2an 691 |
. . . . . . . . . 10
β’ ((π§ β V β¦ πΊ)β(π» βΎ π)) = β¦(π» βΎ π) / π§β¦πΊ |
113 | 26 | reseq1i 5934 |
. . . . . . . . . . 11
β’ (π» βΎ π) = (recs((π§ β V β¦ πΊ)) βΎ π) |
114 | 113 | fveq2i 6846 |
. . . . . . . . . 10
β’ ((π§ β V β¦ πΊ)β(π» βΎ π)) = ((π§ β V β¦ πΊ)β(recs((π§ β V β¦ πΊ)) βΎ π)) |
115 | 112, 114 | eqtr3i 2767 |
. . . . . . . . 9
β’
β¦(π»
βΎ π) / π§β¦πΊ = ((π§ β V β¦ πΊ)β(recs((π§ β V β¦ πΊ)) βΎ π)) |
116 | 103, 104,
115 | 3eqtr4g 2802 |
. . . . . . . 8
β’ (π β On β (π»βπ) = β¦(π» βΎ π) / π§β¦πΊ) |
117 | | weeq1 5622 |
. . . . . . . 8
β’ ((π»βπ) = β¦(π» βΎ π) / π§β¦πΊ β ((π»βπ) We (π
1βπ) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ))) |
118 | 116, 117 | syl 17 |
. . . . . . 7
β’ (π β On β ((π»βπ) We (π
1βπ) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ))) |
119 | 118 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β ((π»βπ) We (π
1βπ) β β¦(π» βΎ π) / π§β¦πΊ We (π
1βπ))) |
120 | 102, 119 | mpbird 257 |
. . . . 5
β’ ((π β On β§ βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β§ (π β§ π β π΄)) β (π»βπ) We (π
1βπ)) |
121 | 120 | 3exp 1120 |
. . . 4
β’ (π β On β (βπ β π ((π β§ π β π΄) β (π»βπ) We (π
1βπ)) β ((π β§ π β π΄) β (π»βπ) We (π
1βπ)))) |
122 | 9, 15, 121 | tfis3 7795 |
. . 3
β’ (π΄ β On β ((π β§ π΄ β π΄) β (π»βπ΄) We (π
1βπ΄))) |
123 | 3, 122 | mpcom 38 |
. 2
β’ ((π β§ π΄ β π΄) β (π»βπ΄) We (π
1βπ΄)) |
124 | 1, 123 | mpan2 690 |
1
β’ (π β (π»βπ΄) We (π
1βπ΄)) |