Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | efgval.r |
. . 3
β’ βΌ = (
~FG βπΌ) |
3 | | efgval2.m |
. . 3
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
4 | | efgval2.t |
. . 3
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
5 | 1, 2, 3, 4 | efgval2 19506 |
. 2
β’ βΌ =
β© {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} |
6 | | efgrelexlem.1 |
. . . . . . . 8
β’ πΏ = {β¨π, πβ© β£ βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)} |
7 | 6 | relopabiv 5776 |
. . . . . . 7
β’ Rel πΏ |
8 | 7 | a1i 11 |
. . . . . 6
β’ (β€
β Rel πΏ) |
9 | | simpr 485 |
. . . . . . 7
β’
((β€ β§ ππΏπ) β ππΏπ) |
10 | | eqcom 2743 |
. . . . . . . . . 10
β’ ((πβ0) = (πβ0) β (πβ0) = (πβ0)) |
11 | 10 | 2rexbii 3128 |
. . . . . . . . 9
β’
(βπ β
(β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
12 | | rexcom 3273 |
. . . . . . . . 9
β’
(βπ β
(β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
13 | 11, 12 | bitri 274 |
. . . . . . . 8
β’
(βπ β
(β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
14 | | efgred.d |
. . . . . . . . 9
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
15 | | efgred.s |
. . . . . . . . 9
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
16 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19531 |
. . . . . . . 8
β’ (ππΏπ β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
17 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19531 |
. . . . . . . 8
β’ (ππΏπ β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
18 | 13, 16, 17 | 3bitr4i 302 |
. . . . . . 7
β’ (ππΏπ β ππΏπ) |
19 | 9, 18 | sylib 217 |
. . . . . 6
β’
((β€ β§ ππΏπ) β ππΏπ) |
20 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19531 |
. . . . . . . . 9
β’ (ππΏβ β βπ β (β‘π β {π})βπ β (β‘π β {β})(πβ0) = (π β0)) |
21 | | reeanv 3217 |
. . . . . . . . . 10
β’
(βπ β
(β‘π β {π})βπ β (β‘π β {π})(βπ β (β‘π β {π})(πβ0) = (πβ0) β§ βπ β (β‘π β {β})(πβ0) = (π β0)) β (βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β§ βπ β (β‘π β {π})βπ β (β‘π β {β})(πβ0) = (π β0))) |
22 | 1, 2, 3, 4, 14, 15 | efgsfo 19521 |
. . . . . . . . . . . . . . . . . . . 20
β’ π:dom πβontoβπ |
23 | | fofn 6758 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π:dom πβontoβπ β π Fn dom π) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ π Fn dom π |
25 | | fniniseg 7010 |
. . . . . . . . . . . . . . . . . . 19
β’ (π Fn dom π β (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π))) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π)) |
27 | | fniniseg 7010 |
. . . . . . . . . . . . . . . . . . 19
β’ (π Fn dom π β (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π))) |
28 | 24, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π)) |
29 | | eqtr3 2762 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβπ) = π β§ (πβπ) = π) β (πβπ) = (πβπ)) |
30 | 1, 2, 3, 4, 14, 15 | efgred 19530 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β dom π β§ π β dom π β§ (πβπ) = (πβπ)) β (πβ0) = (πβ0)) |
31 | 30 | eqcomd 2742 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β dom π β§ π β dom π β§ (πβπ) = (πβπ)) β (πβ0) = (πβ0)) |
32 | 31 | 3expa 1118 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β dom π β§ π β dom π) β§ (πβπ) = (πβπ)) β (πβ0) = (πβ0)) |
33 | 29, 32 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β dom π β§ π β dom π) β§ ((πβπ) = π β§ (πβπ) = π)) β (πβ0) = (πβ0)) |
34 | 33 | an4s 658 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β dom π β§ (πβπ) = π) β§ (π β dom π β§ (πβπ) = π)) β (πβ0) = (πβ0)) |
35 | 26, 28, 34 | syl2anb 598 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (β‘π β {π}) β§ π β (β‘π β {π})) β (πβ0) = (πβ0)) |
36 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . 17
β’ ((πβ0) = (π β0) β ((πβ0) = (πβ0) β (πβ0) = (π β0))) |
37 | 35, 36 | syl5ibcom 244 |
. . . . . . . . . . . . . . . 16
β’ ((π β (β‘π β {π}) β§ π β (β‘π β {π})) β ((πβ0) = (π β0) β (πβ0) = (π β0))) |
38 | 37 | reximdv 3167 |
. . . . . . . . . . . . . . 15
β’ ((π β (β‘π β {π}) β§ π β (β‘π β {π})) β (βπ β (β‘π β {β})(πβ0) = (π β0) β βπ β (β‘π β {β})(πβ0) = (π β0))) |
39 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . 17
β’ ((πβ0) = (πβ0) β ((πβ0) = (π β0) β (πβ0) = (π β0))) |
40 | 39 | rexbidv 3175 |
. . . . . . . . . . . . . . . 16
β’ ((πβ0) = (πβ0) β (βπ β (β‘π β {β})(πβ0) = (π β0) β βπ β (β‘π β {β})(πβ0) = (π β0))) |
41 | 40 | imbi2d 340 |
. . . . . . . . . . . . . . 15
β’ ((πβ0) = (πβ0) β ((βπ β (β‘π β {β})(πβ0) = (π β0) β βπ β (β‘π β {β})(πβ0) = (π β0)) β (βπ β (β‘π β {β})(πβ0) = (π β0) β βπ β (β‘π β {β})(πβ0) = (π β0)))) |
42 | 38, 41 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
β’ ((π β (β‘π β {π}) β§ π β (β‘π β {π})) β ((πβ0) = (πβ0) β (βπ β (β‘π β {β})(πβ0) = (π β0) β βπ β (β‘π β {β})(πβ0) = (π β0)))) |
43 | 42 | rexlimdva 3152 |
. . . . . . . . . . . . 13
β’ (π β (β‘π β {π}) β (βπ β (β‘π β {π})(πβ0) = (πβ0) β (βπ β (β‘π β {β})(πβ0) = (π β0) β βπ β (β‘π β {β})(πβ0) = (π β0)))) |
44 | 43 | impd 411 |
. . . . . . . . . . . 12
β’ (π β (β‘π β {π}) β ((βπ β (β‘π β {π})(πβ0) = (πβ0) β§ βπ β (β‘π β {β})(πβ0) = (π β0)) β βπ β (β‘π β {β})(πβ0) = (π β0))) |
45 | 44 | rexlimiv 3145 |
. . . . . . . . . . 11
β’
(βπ β
(β‘π β {π})(βπ β (β‘π β {π})(πβ0) = (πβ0) β§ βπ β (β‘π β {β})(πβ0) = (π β0)) β βπ β (β‘π β {β})(πβ0) = (π β0)) |
46 | 45 | reximi 3087 |
. . . . . . . . . 10
β’
(βπ β
(β‘π β {π})βπ β (β‘π β {π})(βπ β (β‘π β {π})(πβ0) = (πβ0) β§ βπ β (β‘π β {β})(πβ0) = (π β0)) β βπ β (β‘π β {π})βπ β (β‘π β {β})(πβ0) = (π β0)) |
47 | 21, 46 | sylbir 234 |
. . . . . . . . 9
β’
((βπ β
(β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β§ βπ β (β‘π β {π})βπ β (β‘π β {β})(πβ0) = (π β0)) β βπ β (β‘π β {π})βπ β (β‘π β {β})(πβ0) = (π β0)) |
48 | 16, 20, 47 | syl2anb 598 |
. . . . . . . 8
β’ ((ππΏπ β§ ππΏβ) β βπ β (β‘π β {π})βπ β (β‘π β {β})(πβ0) = (π β0)) |
49 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19531 |
. . . . . . . 8
β’ (ππΏβ β βπ β (β‘π β {π})βπ β (β‘π β {β})(πβ0) = (π β0)) |
50 | 48, 49 | sylibr 233 |
. . . . . . 7
β’ ((ππΏπ β§ ππΏβ) β ππΏβ) |
51 | 50 | adantl 482 |
. . . . . 6
β’
((β€ β§ (ππΏπ β§ ππΏβ)) β ππΏβ) |
52 | | eqid 2736 |
. . . . . . . . . . . 12
β’ (πβ0) = (πβ0) |
53 | | fveq1 6841 |
. . . . . . . . . . . . 13
β’ (π = π β (πβ0) = (πβ0)) |
54 | 53 | rspceeqv 3595 |
. . . . . . . . . . . 12
β’ ((π β (β‘π β {π}) β§ (πβ0) = (πβ0)) β βπ β (β‘π β {π})(πβ0) = (πβ0)) |
55 | 52, 54 | mpan2 689 |
. . . . . . . . . . 11
β’ (π β (β‘π β {π}) β βπ β (β‘π β {π})(πβ0) = (πβ0)) |
56 | 55 | pm4.71i 560 |
. . . . . . . . . 10
β’ (π β (β‘π β {π}) β (π β (β‘π β {π}) β§ βπ β (β‘π β {π})(πβ0) = (πβ0))) |
57 | | fniniseg 7010 |
. . . . . . . . . . 11
β’ (π Fn dom π β (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π))) |
58 | 24, 57 | ax-mp 5 |
. . . . . . . . . 10
β’ (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π)) |
59 | 56, 58 | bitr3i 276 |
. . . . . . . . 9
β’ ((π β (β‘π β {π}) β§ βπ β (β‘π β {π})(πβ0) = (πβ0)) β (π β dom π β§ (πβπ) = π)) |
60 | 59 | rexbii2 3093 |
. . . . . . . 8
β’
(βπ β
(β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β dom π(πβπ) = π) |
61 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19531 |
. . . . . . . 8
β’ (ππΏπ β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
62 | | forn 6759 |
. . . . . . . . . . 11
β’ (π:dom πβontoβπ β ran π = π) |
63 | 22, 62 | ax-mp 5 |
. . . . . . . . . 10
β’ ran π = π |
64 | 63 | eleq2i 2829 |
. . . . . . . . 9
β’ (π β ran π β π β π) |
65 | | fvelrnb 6903 |
. . . . . . . . . 10
β’ (π Fn dom π β (π β ran π β βπ β dom π(πβπ) = π)) |
66 | 24, 65 | ax-mp 5 |
. . . . . . . . 9
β’ (π β ran π β βπ β dom π(πβπ) = π) |
67 | 64, 66 | bitr3i 276 |
. . . . . . . 8
β’ (π β π β βπ β dom π(πβπ) = π) |
68 | 60, 61, 67 | 3bitr4ri 303 |
. . . . . . 7
β’ (π β π β ππΏπ) |
69 | 68 | a1i 11 |
. . . . . 6
β’ (β€
β (π β π β ππΏπ)) |
70 | 8, 19, 51, 69 | iserd 8674 |
. . . . 5
β’ (β€
β πΏ Er π) |
71 | 70 | mptru 1548 |
. . . 4
β’ πΏ Er π |
72 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π β π β§ π β ran (πβπ)) β π β π) |
73 | | foelrn 7056 |
. . . . . . . . . . 11
β’ ((π:dom πβontoβπ β§ π β π) β βπ β dom π π = (πβπ)) |
74 | 22, 72, 73 | sylancr 587 |
. . . . . . . . . 10
β’ ((π β π β§ π β ran (πβπ)) β βπ β dom π π = (πβπ)) |
75 | | simprl 769 |
. . . . . . . . . . 11
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π β dom π) |
76 | | simprr 771 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π = (πβπ)) |
77 | 76 | eqcomd 2742 |
. . . . . . . . . . 11
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β (πβπ) = π) |
78 | | fniniseg 7010 |
. . . . . . . . . . . 12
β’ (π Fn dom π β (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π))) |
79 | 24, 78 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π)) |
80 | 75, 77, 79 | sylanbrc 583 |
. . . . . . . . . 10
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π β (β‘π β {π})) |
81 | | simplr 767 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π β ran (πβπ)) |
82 | 76 | fveq2d 6846 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β (πβπ) = (πβ(πβπ))) |
83 | 82 | rneqd 5893 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β ran (πβπ) = ran (πβ(πβπ))) |
84 | 81, 83 | eleqtrd 2839 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π β ran (πβ(πβπ))) |
85 | 1, 2, 3, 4, 14, 15 | efgsp1 19519 |
. . . . . . . . . . . . 13
β’ ((π β dom π β§ π β ran (πβ(πβπ))) β (π ++ β¨βπββ©) β dom π) |
86 | 75, 84, 85 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β (π ++ β¨βπββ©) β dom π) |
87 | 1, 2, 3, 4, 14, 15 | efgsdm 19512 |
. . . . . . . . . . . . . . . 16
β’ (π β dom π β (π β (Word π β {β
}) β§ (πβ0) β π· β§ βπ β
(1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))))) |
88 | 87 | simp1bi 1145 |
. . . . . . . . . . . . . . 15
β’ (π β dom π β π β (Word π β {β
})) |
89 | 88 | ad2antrl 726 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π β (Word π β {β
})) |
90 | 89 | eldifad 3922 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π β Word π) |
91 | 1, 2, 3, 4 | efgtf 19504 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β ((πβπ) = (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ)) |
92 | 91 | simprd 496 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ) |
93 | 92 | frnd 6676 |
. . . . . . . . . . . . . . 15
β’ (π β π β ran (πβπ) β π) |
94 | 93 | sselda 3944 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β ran (πβπ)) β π β π) |
95 | 94 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β π β π) |
96 | 1, 2, 3, 4, 14, 15 | efgsval2 19515 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ π β π β§ (π ++ β¨βπββ©) β dom π) β (πβ(π ++ β¨βπββ©)) = π) |
97 | 90, 95, 86, 96 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β (πβ(π ++ β¨βπββ©)) = π) |
98 | | fniniseg 7010 |
. . . . . . . . . . . . 13
β’ (π Fn dom π β ((π ++ β¨βπββ©) β (β‘π β {π}) β ((π ++ β¨βπββ©) β dom π β§ (πβ(π ++ β¨βπββ©)) = π))) |
99 | 24, 98 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π ++ β¨βπββ©) β (β‘π β {π}) β ((π ++ β¨βπββ©) β dom π β§ (πβ(π ++ β¨βπββ©)) = π)) |
100 | 86, 97, 99 | sylanbrc 583 |
. . . . . . . . . . 11
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β (π ++ β¨βπββ©) β (β‘π β {π})) |
101 | 95 | s1cld 14491 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β β¨βπββ© β Word π) |
102 | | eldifsn 4747 |
. . . . . . . . . . . . . . . 16
β’ (π β (Word π β {β
}) β (π β Word π β§ π β β
)) |
103 | | lennncl 14422 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word π β§ π β β
) β (β―βπ) β
β) |
104 | 102, 103 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π β (Word π β {β
}) β
(β―βπ) β
β) |
105 | 89, 104 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β (β―βπ) β β) |
106 | | lbfzo0 13612 |
. . . . . . . . . . . . . 14
β’ (0 β
(0..^(β―βπ))
β (β―βπ)
β β) |
107 | 105, 106 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β 0 β (0..^(β―βπ))) |
108 | | ccatval1 14465 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ β¨βπββ© β Word π β§ 0 β (0..^(β―βπ))) β ((π ++ β¨βπββ©)β0) = (πβ0)) |
109 | 90, 101, 107, 108 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β ((π ++ β¨βπββ©)β0) = (πβ0)) |
110 | 109 | eqcomd 2742 |
. . . . . . . . . . 11
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β (πβ0) = ((π ++ β¨βπββ©)β0)) |
111 | | fveq1 6841 |
. . . . . . . . . . . 12
β’ (π = (π ++ β¨βπββ©) β (π β0) = ((π ++ β¨βπββ©)β0)) |
112 | 111 | rspceeqv 3595 |
. . . . . . . . . . 11
β’ (((π ++ β¨βπββ©) β (β‘π β {π}) β§ (πβ0) = ((π ++ β¨βπββ©)β0)) β βπ β (β‘π β {π})(πβ0) = (π β0)) |
113 | 100, 110,
112 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ π = (πβπ))) β βπ β (β‘π β {π})(πβ0) = (π β0)) |
114 | 74, 80, 113 | reximssdv 3169 |
. . . . . . . . 9
β’ ((π β π β§ π β ran (πβπ)) β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (π β0)) |
115 | 1, 2, 3, 4, 14, 15, 6 | efgrelexlema 19531 |
. . . . . . . . 9
β’ (ππΏπ β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (π β0)) |
116 | 114, 115 | sylibr 233 |
. . . . . . . 8
β’ ((π β π β§ π β ran (πβπ)) β ππΏπ) |
117 | | vex 3449 |
. . . . . . . . 9
β’ π β V |
118 | | vex 3449 |
. . . . . . . . 9
β’ π β V |
119 | 117, 118 | elec 8692 |
. . . . . . . 8
β’ (π β [π]πΏ β ππΏπ) |
120 | 116, 119 | sylibr 233 |
. . . . . . 7
β’ ((π β π β§ π β ran (πβπ)) β π β [π]πΏ) |
121 | 120 | ex 413 |
. . . . . 6
β’ (π β π β (π β ran (πβπ) β π β [π]πΏ)) |
122 | 121 | ssrdv 3950 |
. . . . 5
β’ (π β π β ran (πβπ) β [π]πΏ) |
123 | 122 | rgen 3066 |
. . . 4
β’
βπ β
π ran (πβπ) β [π]πΏ |
124 | 1 | fvexi 6856 |
. . . . . 6
β’ π β V |
125 | | erex 8672 |
. . . . . 6
β’ (πΏ Er π β (π β V β πΏ β V)) |
126 | 71, 124, 125 | mp2 9 |
. . . . 5
β’ πΏ β V |
127 | | ereq1 8655 |
. . . . . 6
β’ (π = πΏ β (π Er π β πΏ Er π)) |
128 | | eceq2 8688 |
. . . . . . . 8
β’ (π = πΏ β [π]π = [π]πΏ) |
129 | 128 | sseq2d 3976 |
. . . . . . 7
β’ (π = πΏ β (ran (πβπ) β [π]π β ran (πβπ) β [π]πΏ)) |
130 | 129 | ralbidv 3174 |
. . . . . 6
β’ (π = πΏ β (βπ β π ran (πβπ) β [π]π β βπ β π ran (πβπ) β [π]πΏ)) |
131 | 127, 130 | anbi12d 631 |
. . . . 5
β’ (π = πΏ β ((π Er π β§ βπ β π ran (πβπ) β [π]π) β (πΏ Er π β§ βπ β π ran (πβπ) β [π]πΏ))) |
132 | 126, 131 | elab 3630 |
. . . 4
β’ (πΏ β {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β (πΏ Er π β§ βπ β π ran (πβπ) β [π]πΏ)) |
133 | 71, 123, 132 | mpbir2an 709 |
. . 3
β’ πΏ β {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} |
134 | | intss1 4924 |
. . 3
β’ (πΏ β {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β β© {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β πΏ) |
135 | 133, 134 | ax-mp 5 |
. 2
β’ β© {π
β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β πΏ |
136 | 5, 135 | eqsstri 3978 |
1
β’ βΌ
β πΏ |