Step | Hyp | Ref
| Expression |
1 | | dyadmbl.1 |
. . 3
β’ πΉ = (π₯ β β€, π¦ β β0 β¦
β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) |
2 | | dyadmbl.2 |
. . 3
β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} |
3 | | dyadmbl.3 |
. . 3
β’ (π β π΄ β ran πΉ) |
4 | 1, 2, 3 | dyadmbllem 24963 |
. 2
β’ (π β βͺ ([,] β π΄) = βͺ ([,]
β πΊ)) |
5 | | isfinite 9588 |
. . . 4
β’ (πΊ β Fin β πΊ βΊ
Ο) |
6 | | iccf 13365 |
. . . . . 6
β’
[,]:(β* Γ β*)βΆπ«
β* |
7 | | ffun 6671 |
. . . . . 6
β’
([,]:(β* Γ β*)βΆπ«
β* β Fun [,]) |
8 | | funiunfv 7195 |
. . . . . 6
β’ (Fun [,]
β βͺ π β πΊ ([,]βπ) = βͺ ([,] β
πΊ)) |
9 | 6, 7, 8 | mp2b 10 |
. . . . 5
β’ βͺ π β πΊ ([,]βπ) = βͺ ([,] β
πΊ) |
10 | | simpr 485 |
. . . . . 6
β’ ((π β§ πΊ β Fin) β πΊ β Fin) |
11 | 2 | ssrab3 4040 |
. . . . . . . . . . . . . . 15
β’ πΊ β π΄ |
12 | 11, 3 | sstrid 3955 |
. . . . . . . . . . . . . 14
β’ (π β πΊ β ran πΉ) |
13 | 1 | dyadf 24955 |
. . . . . . . . . . . . . . . 16
β’ πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ
β)) |
14 | | frn 6675 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ β)) β ran
πΉ β ( β€ β©
(β Γ β))) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ran πΉ β ( β€ β© (β
Γ β)) |
16 | | inss2 4189 |
. . . . . . . . . . . . . . 15
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
17 | 15, 16 | sstri 3953 |
. . . . . . . . . . . . . 14
β’ ran πΉ β (β Γ
β) |
18 | 12, 17 | sstrdi 3956 |
. . . . . . . . . . . . 13
β’ (π β πΊ β (β Γ
β)) |
19 | 18 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ πΊ β Fin) β πΊ β (β Γ
β)) |
20 | 19 | sselda 3944 |
. . . . . . . . . . 11
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β π β (β Γ
β)) |
21 | | 1st2nd2 7960 |
. . . . . . . . . . 11
β’ (π β (β Γ
β) β π =
β¨(1st βπ), (2nd βπ)β©) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β π = β¨(1st βπ), (2nd βπ)β©) |
23 | 22 | fveq2d 6846 |
. . . . . . . . 9
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β ([,]βπ) = ([,]ββ¨(1st
βπ), (2nd
βπ)β©)) |
24 | | df-ov 7360 |
. . . . . . . . 9
β’
((1st βπ)[,](2nd βπ)) = ([,]ββ¨(1st
βπ), (2nd
βπ)β©) |
25 | 23, 24 | eqtr4di 2794 |
. . . . . . . 8
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β ([,]βπ) = ((1st βπ)[,](2nd βπ))) |
26 | | xp1st 7953 |
. . . . . . . . . 10
β’ (π β (β Γ
β) β (1st βπ) β β) |
27 | 20, 26 | syl 17 |
. . . . . . . . 9
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β (1st βπ) β
β) |
28 | | xp2nd 7954 |
. . . . . . . . . 10
β’ (π β (β Γ
β) β (2nd βπ) β β) |
29 | 20, 28 | syl 17 |
. . . . . . . . 9
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β (2nd βπ) β
β) |
30 | | iccmbl 24930 |
. . . . . . . . 9
β’
(((1st βπ) β β β§ (2nd
βπ) β β)
β ((1st βπ)[,](2nd βπ)) β dom vol) |
31 | 27, 29, 30 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β ((1st βπ)[,](2nd βπ)) β dom
vol) |
32 | 25, 31 | eqeltrd 2837 |
. . . . . . 7
β’ (((π β§ πΊ β Fin) β§ π β πΊ) β ([,]βπ) β dom vol) |
33 | 32 | ralrimiva 3143 |
. . . . . 6
β’ ((π β§ πΊ β Fin) β βπ β πΊ ([,]βπ) β dom vol) |
34 | | finiunmbl 24908 |
. . . . . 6
β’ ((πΊ β Fin β§ βπ β πΊ ([,]βπ) β dom vol) β βͺ π β πΊ ([,]βπ) β dom vol) |
35 | 10, 33, 34 | syl2anc 584 |
. . . . 5
β’ ((π β§ πΊ β Fin) β βͺ π β πΊ ([,]βπ) β dom vol) |
36 | 9, 35 | eqeltrrid 2842 |
. . . 4
β’ ((π β§ πΊ β Fin) β βͺ ([,] β πΊ) β dom vol) |
37 | 5, 36 | sylan2br 595 |
. . 3
β’ ((π β§ πΊ βΊ Ο) β βͺ ([,] β πΊ) β dom vol) |
38 | | rnco2 6205 |
. . . . . . . . 9
β’ ran ([,]
β π) = ([,] β
ran π) |
39 | | f1ofo 6791 |
. . . . . . . . . . . 12
β’ (π:ββ1-1-ontoβπΊ β π:ββontoβπΊ) |
40 | 39 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π:ββ1-1-ontoβπΊ) β π:ββontoβπΊ) |
41 | | forn 6759 |
. . . . . . . . . . 11
β’ (π:ββontoβπΊ β ran π = πΊ) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π:ββ1-1-ontoβπΊ) β ran π = πΊ) |
43 | 42 | imaeq2d 6013 |
. . . . . . . . 9
β’ ((π β§ π:ββ1-1-ontoβπΊ) β ([,] β ran π) = ([,] β πΊ)) |
44 | 38, 43 | eqtrid 2788 |
. . . . . . . 8
β’ ((π β§ π:ββ1-1-ontoβπΊ) β ran ([,] β π) = ([,] β πΊ)) |
45 | 44 | unieqd 4879 |
. . . . . . 7
β’ ((π β§ π:ββ1-1-ontoβπΊ) β βͺ ran ([,] β π) = βͺ ([,] β
πΊ)) |
46 | | f1of 6784 |
. . . . . . . . 9
β’ (π:ββ1-1-ontoβπΊ β π:ββΆπΊ) |
47 | 12, 15 | sstrdi 3956 |
. . . . . . . . 9
β’ (π β πΊ β ( β€ β© (β Γ
β))) |
48 | | fss 6685 |
. . . . . . . . 9
β’ ((π:ββΆπΊ β§ πΊ β ( β€ β© (β Γ
β))) β π:ββΆ( β€ β© (β Γ
β))) |
49 | 46, 47, 48 | syl2anr 597 |
. . . . . . . 8
β’ ((π β§ π:ββ1-1-ontoβπΊ) β π:ββΆ( β€ β© (β Γ
β))) |
50 | | fss 6685 |
. . . . . . . . . . . . . 14
β’ ((π:ββΆπΊ β§ πΊ β ran πΉ) β π:ββΆran πΉ) |
51 | 46, 12, 50 | syl2anr 597 |
. . . . . . . . . . . . 13
β’ ((π β§ π:ββ1-1-ontoβπΊ) β π:ββΆran πΉ) |
52 | | simpl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β π β
β) |
53 | | ffvelcdm 7032 |
. . . . . . . . . . . . 13
β’ ((π:ββΆran πΉ β§ π β β) β (πβπ) β ran πΉ) |
54 | 51, 52, 53 | syl2an 596 |
. . . . . . . . . . . 12
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (πβπ) β ran πΉ) |
55 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β π β
β) |
56 | | ffvelcdm 7032 |
. . . . . . . . . . . . 13
β’ ((π:ββΆran πΉ β§ π β β) β (πβπ) β ran πΉ) |
57 | 51, 55, 56 | syl2an 596 |
. . . . . . . . . . . 12
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (πβπ) β ran πΉ) |
58 | 1 | dyaddisj 24960 |
. . . . . . . . . . . 12
β’ (((πβπ) β ran πΉ β§ (πβπ) β ran πΉ) β (([,]β(πβπ)) β ([,]β(πβπ)) β¨ ([,]β(πβπ)) β ([,]β(πβπ)) β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
)) |
59 | 54, 57, 58 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (([,]β(πβπ)) β ([,]β(πβπ)) β¨ ([,]β(πβπ)) β ([,]β(πβπ)) β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
)) |
60 | | fveq2 6842 |
. . . . . . . . . . . . . . . 16
β’ (π€ = (πβπ) β ([,]βπ€) = ([,]β(πβπ))) |
61 | 60 | sseq2d 3976 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πβπ) β (([,]β(πβπ)) β ([,]βπ€) β ([,]β(πβπ)) β ([,]β(πβπ)))) |
62 | | eqeq2 2748 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πβπ) β ((πβπ) = π€ β (πβπ) = (πβπ))) |
63 | 61, 62 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π€ = (πβπ) β ((([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€) β (([,]β(πβπ)) β ([,]β(πβπ)) β (πβπ) = (πβπ)))) |
64 | 46 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π:ββ1-1-ontoβπΊ) β π:ββΆπΊ) |
65 | | ffvelcdm 7032 |
. . . . . . . . . . . . . . . 16
β’ ((π:ββΆπΊ β§ π β β) β (πβπ) β πΊ) |
66 | 64, 52, 65 | syl2an 596 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (πβπ) β πΊ) |
67 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = (πβπ) β ([,]βπ§) = ([,]β(πβπ))) |
68 | 67 | sseq1d 3975 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (πβπ) β (([,]βπ§) β ([,]βπ€) β ([,]β(πβπ)) β ([,]βπ€))) |
69 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (πβπ) β (π§ = π€ β (πβπ) = π€)) |
70 | 68, 69 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (πβπ) β ((([,]βπ§) β ([,]βπ€) β π§ = π€) β (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€))) |
71 | 70 | ralbidv 3174 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (πβπ) β (βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€) β βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€))) |
72 | 71, 2 | elrab2 3648 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β πΊ β ((πβπ) β π΄ β§ βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€))) |
73 | 72 | simprbi 497 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β πΊ β βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€)) |
74 | 66, 73 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€)) |
75 | | ffvelcdm 7032 |
. . . . . . . . . . . . . . . 16
β’ ((π:ββΆπΊ β§ π β β) β (πβπ) β πΊ) |
76 | 64, 55, 75 | syl2an 596 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (πβπ) β πΊ) |
77 | 11, 76 | sselid 3942 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (πβπ) β π΄) |
78 | 63, 74, 77 | rspcdva 3582 |
. . . . . . . . . . . . 13
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (([,]β(πβπ)) β ([,]β(πβπ)) β (πβπ) = (πβπ))) |
79 | | f1of1 6783 |
. . . . . . . . . . . . . . . 16
β’ (π:ββ1-1-ontoβπΊ β π:ββ1-1βπΊ) |
80 | 79 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π:ββ1-1-ontoβπΊ) β π:ββ1-1βπΊ) |
81 | | f1fveq 7209 |
. . . . . . . . . . . . . . 15
β’ ((π:ββ1-1βπΊ β§ (π β β β§ π β β)) β ((πβπ) = (πβπ) β π = π)) |
82 | 80, 81 | sylan 580 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β ((πβπ) = (πβπ) β π = π)) |
83 | | orc 865 |
. . . . . . . . . . . . . 14
β’ (π = π β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
)) |
84 | 82, 83 | syl6bi 252 |
. . . . . . . . . . . . 13
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β ((πβπ) = (πβπ) β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
))) |
85 | 78, 84 | syld 47 |
. . . . . . . . . . . 12
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (([,]β(πβπ)) β ([,]β(πβπ)) β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
))) |
86 | | fveq2 6842 |
. . . . . . . . . . . . . . . 16
β’ (π€ = (πβπ) β ([,]βπ€) = ([,]β(πβπ))) |
87 | 86 | sseq2d 3976 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πβπ) β (([,]β(πβπ)) β ([,]βπ€) β ([,]β(πβπ)) β ([,]β(πβπ)))) |
88 | | eqeq2 2748 |
. . . . . . . . . . . . . . . 16
β’ (π€ = (πβπ) β ((πβπ) = π€ β (πβπ) = (πβπ))) |
89 | | eqcom 2743 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) = (πβπ) β (πβπ) = (πβπ)) |
90 | 88, 89 | bitrdi 286 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πβπ) β ((πβπ) = π€ β (πβπ) = (πβπ))) |
91 | 87, 90 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π€ = (πβπ) β ((([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€) β (([,]β(πβπ)) β ([,]β(πβπ)) β (πβπ) = (πβπ)))) |
92 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = (πβπ) β ([,]βπ§) = ([,]β(πβπ))) |
93 | 92 | sseq1d 3975 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (πβπ) β (([,]βπ§) β ([,]βπ€) β ([,]β(πβπ)) β ([,]βπ€))) |
94 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (πβπ) β (π§ = π€ β (πβπ) = π€)) |
95 | 93, 94 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (πβπ) β ((([,]βπ§) β ([,]βπ€) β π§ = π€) β (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€))) |
96 | 95 | ralbidv 3174 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (πβπ) β (βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€) β βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€))) |
97 | 96, 2 | elrab2 3648 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β πΊ β ((πβπ) β π΄ β§ βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€))) |
98 | 97 | simprbi 497 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β πΊ β βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€)) |
99 | 76, 98 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β βπ€ β π΄ (([,]β(πβπ)) β ([,]βπ€) β (πβπ) = π€)) |
100 | 11, 66 | sselid 3942 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (πβπ) β π΄) |
101 | 91, 99, 100 | rspcdva 3582 |
. . . . . . . . . . . . 13
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (([,]β(πβπ)) β ([,]β(πβπ)) β (πβπ) = (πβπ))) |
102 | 101, 84 | syld 47 |
. . . . . . . . . . . 12
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (([,]β(πβπ)) β ([,]β(πβπ)) β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
))) |
103 | | olc 866 |
. . . . . . . . . . . . 13
β’
((((,)β(πβπ)) β© ((,)β(πβπ))) = β
β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
)) |
104 | 103 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β ((((,)β(πβπ)) β© ((,)β(πβπ))) = β
β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
))) |
105 | 85, 102, 104 | 3jaod 1428 |
. . . . . . . . . . 11
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β ((([,]β(πβπ)) β ([,]β(πβπ)) β¨ ([,]β(πβπ)) β ([,]β(πβπ)) β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
) β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
))) |
106 | 59, 105 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ π:ββ1-1-ontoβπΊ) β§ (π β β β§ π β β)) β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
)) |
107 | 106 | ralrimivva 3197 |
. . . . . . . . 9
β’ ((π β§ π:ββ1-1-ontoβπΊ) β βπ β β βπ β β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
)) |
108 | | 2fveq3 6847 |
. . . . . . . . . 10
β’ (π = π β ((,)β(πβπ)) = ((,)β(πβπ))) |
109 | 108 | disjor 5085 |
. . . . . . . . 9
β’
(Disj π
β β ((,)β(πβπ)) β βπ β β βπ β β (π = π β¨ (((,)β(πβπ)) β© ((,)β(πβπ))) = β
)) |
110 | 107, 109 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ π:ββ1-1-ontoβπΊ) β Disj π β β
((,)β(πβπ))) |
111 | | eqid 2736 |
. . . . . . . 8
β’ seq1( + ,
((abs β β ) β π)) = seq1( + , ((abs β β )
β π)) |
112 | 49, 110, 111 | uniiccmbl 24954 |
. . . . . . 7
β’ ((π β§ π:ββ1-1-ontoβπΊ) β βͺ ran ([,] β π) β dom vol) |
113 | 45, 112 | eqeltrrd 2838 |
. . . . . 6
β’ ((π β§ π:ββ1-1-ontoβπΊ) β βͺ ([,] β πΊ) β dom vol) |
114 | 113 | ex 413 |
. . . . 5
β’ (π β (π:ββ1-1-ontoβπΊ β βͺ ([,] β πΊ) β dom vol)) |
115 | 114 | exlimdv 1936 |
. . . 4
β’ (π β (βπ π:ββ1-1-ontoβπΊ β βͺ ([,] β πΊ) β dom vol)) |
116 | | nnenom 13885 |
. . . . . 6
β’ β
β Ο |
117 | | ensym 8943 |
. . . . . 6
β’ (πΊ β Ο β Ο
β πΊ) |
118 | | entr 8946 |
. . . . . 6
β’ ((β
β Ο β§ Ο β πΊ) β β β πΊ) |
119 | 116, 117,
118 | sylancr 587 |
. . . . 5
β’ (πΊ β Ο β β
β πΊ) |
120 | | bren 8893 |
. . . . 5
β’ (β
β πΊ β
βπ π:ββ1-1-ontoβπΊ) |
121 | 119, 120 | sylib 217 |
. . . 4
β’ (πΊ β Ο β
βπ π:ββ1-1-ontoβπΊ) |
122 | 115, 121 | impel 506 |
. . 3
β’ ((π β§ πΊ β Ο) β βͺ ([,] β πΊ) β dom vol) |
123 | | reex 11142 |
. . . . . . . . 9
β’ β
β V |
124 | 123, 123 | xpex 7687 |
. . . . . . . 8
β’ (β
Γ β) β V |
125 | 124 | inex2 5275 |
. . . . . . 7
β’ ( β€
β© (β Γ β)) β V |
126 | 125, 15 | ssexi 5279 |
. . . . . 6
β’ ran πΉ β V |
127 | | ssdomg 8940 |
. . . . . 6
β’ (ran
πΉ β V β (πΊ β ran πΉ β πΊ βΌ ran πΉ)) |
128 | 126, 12, 127 | mpsyl 68 |
. . . . 5
β’ (π β πΊ βΌ ran πΉ) |
129 | | omelon 9582 |
. . . . . . . 8
β’ Ο
β On |
130 | | znnen 16094 |
. . . . . . . . . . . 12
β’ β€
β β |
131 | 130, 116 | entri 8948 |
. . . . . . . . . . 11
β’ β€
β Ο |
132 | | nn0ennn 13884 |
. . . . . . . . . . . 12
β’
β0 β β |
133 | 132, 116 | entri 8948 |
. . . . . . . . . . 11
β’
β0 β Ο |
134 | | xpen 9084 |
. . . . . . . . . . 11
β’ ((β€
β Ο β§ β0 β Ο) β (β€
Γ β0) β (Ο Γ
Ο)) |
135 | 131, 133,
134 | mp2an 690 |
. . . . . . . . . 10
β’ (β€
Γ β0) β (Ο Γ Ο) |
136 | | xpomen 9951 |
. . . . . . . . . 10
β’ (Ο
Γ Ο) β Ο |
137 | 135, 136 | entri 8948 |
. . . . . . . . 9
β’ (β€
Γ β0) β Ο |
138 | 137 | ensymi 8944 |
. . . . . . . 8
β’ Ο
β (β€ Γ β0) |
139 | | isnumi 9882 |
. . . . . . . 8
β’ ((Ο
β On β§ Ο β (β€ Γ β0)) β
(β€ Γ β0) β dom card) |
140 | 129, 138,
139 | mp2an 690 |
. . . . . . 7
β’ (β€
Γ β0) β dom card |
141 | | ffn 6668 |
. . . . . . . . 9
β’ (πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ β)) β
πΉ Fn (β€ Γ
β0)) |
142 | 13, 141 | ax-mp 5 |
. . . . . . . 8
β’ πΉ Fn (β€ Γ
β0) |
143 | | dffn4 6762 |
. . . . . . . 8
β’ (πΉ Fn (β€ Γ
β0) β πΉ:(β€ Γ
β0)βontoβran
πΉ) |
144 | 142, 143 | mpbi 229 |
. . . . . . 7
β’ πΉ:(β€ Γ
β0)βontoβran
πΉ |
145 | | fodomnum 9993 |
. . . . . . 7
β’ ((β€
Γ β0) β dom card β (πΉ:(β€ Γ
β0)βontoβran
πΉ β ran πΉ βΌ (β€ Γ
β0))) |
146 | 140, 144,
145 | mp2 9 |
. . . . . 6
β’ ran πΉ βΌ (β€ Γ
β0) |
147 | | domentr 8953 |
. . . . . 6
β’ ((ran
πΉ βΌ (β€ Γ
β0) β§ (β€ Γ β0) β
Ο) β ran πΉ
βΌ Ο) |
148 | 146, 137,
147 | mp2an 690 |
. . . . 5
β’ ran πΉ βΌ
Ο |
149 | | domtr 8947 |
. . . . 5
β’ ((πΊ βΌ ran πΉ β§ ran πΉ βΌ Ο) β πΊ βΌ Ο) |
150 | 128, 148,
149 | sylancl 586 |
. . . 4
β’ (π β πΊ βΌ Ο) |
151 | | brdom2 8922 |
. . . 4
β’ (πΊ βΌ Ο β (πΊ βΊ Ο β¨ πΊ β
Ο)) |
152 | 150, 151 | sylib 217 |
. . 3
β’ (π β (πΊ βΊ Ο β¨ πΊ β Ο)) |
153 | 37, 122, 152 | mpjaodan 957 |
. 2
β’ (π β βͺ ([,] β πΊ) β dom vol) |
154 | 4, 153 | eqeltrd 2837 |
1
β’ (π β βͺ ([,] β π΄) β dom vol) |