Step | Hyp | Ref
| Expression |
1 | | eluni2 4874 |
. . . 4
β’ (π β βͺ ([,] β π΄) β βπ β ([,] β π΄)π β π) |
2 | | iccf 13372 |
. . . . . . 7
β’
[,]:(β* Γ β*)βΆπ«
β* |
3 | | ffn 6673 |
. . . . . . 7
β’
([,]:(β* Γ β*)βΆπ«
β* β [,] Fn (β* Γ
β*)) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
β’ [,] Fn
(β* Γ β*) |
5 | | dyadmbl.3 |
. . . . . . 7
β’ (π β π΄ β ran πΉ) |
6 | | dyadmbl.1 |
. . . . . . . . . 10
β’ πΉ = (π₯ β β€, π¦ β β0 β¦
β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) |
7 | 6 | dyadf 24971 |
. . . . . . . . 9
β’ πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ
β)) |
8 | | frn 6680 |
. . . . . . . . 9
β’ (πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ β)) β ran
πΉ β ( β€ β©
(β Γ β))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . 8
β’ ran πΉ β ( β€ β© (β
Γ β)) |
10 | | inss2 4194 |
. . . . . . . . 9
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
11 | | rexpssxrxp 11207 |
. . . . . . . . 9
β’ (β
Γ β) β (β* Γ
β*) |
12 | 10, 11 | sstri 3958 |
. . . . . . . 8
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
13 | 9, 12 | sstri 3958 |
. . . . . . 7
β’ ran πΉ β (β*
Γ β*) |
14 | 5, 13 | sstrdi 3961 |
. . . . . 6
β’ (π β π΄ β (β* Γ
β*)) |
15 | | eleq2 2827 |
. . . . . . 7
β’ (π = ([,]βπ‘) β (π β π β π β ([,]βπ‘))) |
16 | 15 | rexima 7192 |
. . . . . 6
β’ (([,] Fn
(β* Γ β*) β§ π΄ β (β* Γ
β*)) β (βπ β ([,] β π΄)π β π β βπ‘ β π΄ π β ([,]βπ‘))) |
17 | 4, 14, 16 | sylancr 588 |
. . . . 5
β’ (π β (βπ β ([,] β π΄)π β π β βπ‘ β π΄ π β ([,]βπ‘))) |
18 | | ssrab2 4042 |
. . . . . . . . 9
β’ {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β π΄ |
19 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β π΄ β ran πΉ) |
20 | 18, 19 | sstrid 3960 |
. . . . . . . 8
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β ran πΉ) |
21 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β π‘ β π΄) |
22 | | ssid 3971 |
. . . . . . . . . 10
β’
([,]βπ‘)
β ([,]βπ‘) |
23 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π‘ β ([,]βπ) = ([,]βπ‘)) |
24 | 23 | sseq2d 3981 |
. . . . . . . . . . 11
β’ (π = π‘ β (([,]βπ‘) β ([,]βπ) β ([,]βπ‘) β ([,]βπ‘))) |
25 | 24 | rspcev 3584 |
. . . . . . . . . 10
β’ ((π‘ β π΄ β§ ([,]βπ‘) β ([,]βπ‘)) β βπ β π΄ ([,]βπ‘) β ([,]βπ)) |
26 | 21, 22, 25 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β βπ β π΄ ([,]βπ‘) β ([,]βπ)) |
27 | | rabn0 4350 |
. . . . . . . . 9
β’ ({π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β β
β βπ β π΄ ([,]βπ‘) β ([,]βπ)) |
28 | 26, 27 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β β
) |
29 | 6 | dyadmax 24978 |
. . . . . . . 8
β’ (({π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β ran πΉ β§ {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β β
) β βπ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)}βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€)) |
30 | 20, 28, 29 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β βπ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)}βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€)) |
31 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β ([,]βπ) = ([,]βπ)) |
32 | 31 | sseq2d 3981 |
. . . . . . . . . 10
β’ (π = π β (([,]βπ‘) β ([,]βπ) β ([,]βπ‘) β ([,]βπ))) |
33 | 32 | elrab 3650 |
. . . . . . . . 9
β’ (π β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) |
34 | | simprlr 779 |
. . . . . . . . . . . 12
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β ([,]βπ‘) β ([,]βπ)) |
35 | | simplrr 777 |
. . . . . . . . . . . 12
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β π β ([,]βπ‘)) |
36 | 34, 35 | sseldd 3950 |
. . . . . . . . . . 11
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β π β ([,]βπ)) |
37 | | simprll 778 |
. . . . . . . . . . . . 13
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β π β π΄) |
38 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π€ β ([,]βπ) = ([,]βπ€)) |
39 | 38 | sseq2d 3981 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π€ β (([,]βπ‘) β ([,]βπ) β ([,]βπ‘) β ([,]βπ€))) |
40 | 39 | elrab 3650 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β (π€ β π΄ β§ ([,]βπ‘) β ([,]βπ€))) |
41 | 40 | imbi1i 350 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β (([,]βπ) β ([,]βπ€) β π = π€)) β ((π€ β π΄ β§ ([,]βπ‘) β ([,]βπ€)) β (([,]βπ) β ([,]βπ€) β π = π€))) |
42 | | impexp 452 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β π΄ β§ ([,]βπ‘) β ([,]βπ€)) β (([,]βπ) β ([,]βπ€) β π = π€)) β (π€ β π΄ β (([,]βπ‘) β ([,]βπ€) β (([,]βπ) β ([,]βπ€) β π = π€)))) |
43 | 41, 42 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β (([,]βπ) β ([,]βπ€) β π = π€)) β (π€ β π΄ β (([,]βπ‘) β ([,]βπ€) β (([,]βπ) β ([,]βπ€) β π = π€)))) |
44 | | impexp 452 |
. . . . . . . . . . . . . . . . . 18
β’
(((([,]βπ‘)
β ([,]βπ€) β§
([,]βπ) β
([,]βπ€)) β π = π€) β (([,]βπ‘) β ([,]βπ€) β (([,]βπ) β ([,]βπ€) β π = π€))) |
45 | | sstr2 3956 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(([,]βπ‘)
β ([,]βπ)
β (([,]βπ)
β ([,]βπ€)
β ([,]βπ‘)
β ([,]βπ€))) |
46 | 45 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) β (([,]βπ) β ([,]βπ€) β ([,]βπ‘) β ([,]βπ€))) |
47 | 46 | ancrd 553 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) β (([,]βπ) β ([,]βπ€) β (([,]βπ‘) β ([,]βπ€) β§ ([,]βπ) β ([,]βπ€)))) |
48 | 47 | imim1d 82 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) β (((([,]βπ‘) β ([,]βπ€) β§ ([,]βπ) β ([,]βπ€)) β π = π€) β (([,]βπ) β ([,]βπ€) β π = π€))) |
49 | 44, 48 | biimtrrid 242 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) β ((([,]βπ‘) β ([,]βπ€) β (([,]βπ) β ([,]βπ€) β π = π€)) β (([,]βπ) β ([,]βπ€) β π = π€))) |
50 | 49 | imim2d 57 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) β ((π€ β π΄ β (([,]βπ‘) β ([,]βπ€) β (([,]βπ) β ([,]βπ€) β π = π€))) β (π€ β π΄ β (([,]βπ) β ([,]βπ€) β π = π€)))) |
51 | 43, 50 | biimtrid 241 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) β ((π€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β (([,]βπ) β ([,]βπ€) β π = π€)) β (π€ β π΄ β (([,]βπ) β ([,]βπ€) β π = π€)))) |
52 | 51 | ralimdv2 3161 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ (π β π΄ β§ ([,]βπ‘) β ([,]βπ))) β (βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€) β βπ€ β π΄ (([,]βπ) β ([,]βπ€) β π = π€))) |
53 | 52 | impr 456 |
. . . . . . . . . . . . 13
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β βπ€ β π΄ (([,]βπ) β ([,]βπ€) β π = π€)) |
54 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β ([,]βπ§) = ([,]βπ)) |
55 | 54 | sseq1d 3980 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (([,]βπ§) β ([,]βπ€) β ([,]βπ) β ([,]βπ€))) |
56 | | equequ1 2029 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (π§ = π€ β π = π€)) |
57 | 55, 56 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β ((([,]βπ§) β ([,]βπ€) β π§ = π€) β (([,]βπ) β ([,]βπ€) β π = π€))) |
58 | 57 | ralbidv 3175 |
. . . . . . . . . . . . . 14
β’ (π§ = π β (βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€) β βπ€ β π΄ (([,]βπ) β ([,]βπ€) β π = π€))) |
59 | | dyadmbl.2 |
. . . . . . . . . . . . . 14
β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} |
60 | 58, 59 | elrab2 3653 |
. . . . . . . . . . . . 13
β’ (π β πΊ β (π β π΄ β§ βπ€ β π΄ (([,]βπ) β ([,]βπ€) β π = π€))) |
61 | 37, 53, 60 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β π β πΊ) |
62 | | ffun 6676 |
. . . . . . . . . . . . . 14
β’
([,]:(β* Γ β*)βΆπ«
β* β Fun [,]) |
63 | 2, 62 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ Fun
[,] |
64 | 59 | ssrab3 4045 |
. . . . . . . . . . . . . . . 16
β’ πΊ β π΄ |
65 | 64, 14 | sstrid 3960 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ β (β* Γ
β*)) |
66 | 2 | fdmi 6685 |
. . . . . . . . . . . . . . 15
β’ dom [,] =
(β* Γ β*) |
67 | 65, 66 | sseqtrrdi 4000 |
. . . . . . . . . . . . . 14
β’ (π β πΊ β dom [,]) |
68 | 67 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β πΊ β dom [,]) |
69 | | funfvima2 7186 |
. . . . . . . . . . . . 13
β’ ((Fun [,]
β§ πΊ β dom [,])
β (π β πΊ β ([,]βπ) β ([,] β πΊ))) |
70 | 63, 68, 69 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β (π β πΊ β ([,]βπ) β ([,] β πΊ))) |
71 | 61, 70 | mpd 15 |
. . . . . . . . . . 11
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β ([,]βπ) β ([,] β πΊ)) |
72 | | elunii 4875 |
. . . . . . . . . . 11
β’ ((π β ([,]βπ) β§ ([,]βπ) β ([,] β πΊ)) β π β βͺ ([,]
β πΊ)) |
73 | 36, 71, 72 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β§ ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β§ βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€))) β π β βͺ ([,]
β πΊ)) |
74 | 73 | exp32 422 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β ((π β π΄ β§ ([,]βπ‘) β ([,]βπ)) β (βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€) β π β βͺ ([,]
β πΊ)))) |
75 | 33, 74 | biimtrid 241 |
. . . . . . . 8
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β (π β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} β (βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€) β π β βͺ ([,]
β πΊ)))) |
76 | 75 | rexlimdv 3151 |
. . . . . . 7
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β (βπ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)}βπ€ β {π β π΄ β£ ([,]βπ‘) β ([,]βπ)} (([,]βπ) β ([,]βπ€) β π = π€) β π β βͺ ([,]
β πΊ))) |
77 | 30, 76 | mpd 15 |
. . . . . 6
β’ ((π β§ (π‘ β π΄ β§ π β ([,]βπ‘))) β π β βͺ ([,]
β πΊ)) |
78 | 77 | rexlimdvaa 3154 |
. . . . 5
β’ (π β (βπ‘ β π΄ π β ([,]βπ‘) β π β βͺ ([,]
β πΊ))) |
79 | 17, 78 | sylbid 239 |
. . . 4
β’ (π β (βπ β ([,] β π΄)π β π β π β βͺ ([,]
β πΊ))) |
80 | 1, 79 | biimtrid 241 |
. . 3
β’ (π β (π β βͺ ([,]
β π΄) β π β βͺ ([,] β πΊ))) |
81 | 80 | ssrdv 3955 |
. 2
β’ (π β βͺ ([,] β π΄) β βͺ ([,]
β πΊ)) |
82 | | imass2 6059 |
. . . 4
β’ (πΊ β π΄ β ([,] β πΊ) β ([,] β π΄)) |
83 | 64, 82 | ax-mp 5 |
. . 3
β’ ([,]
β πΊ) β ([,]
β π΄) |
84 | | uniss 4878 |
. . 3
β’ (([,]
β πΊ) β ([,]
β π΄) β βͺ ([,] β πΊ) β βͺ ([,]
β π΄)) |
85 | 83, 84 | mp1i 13 |
. 2
β’ (π β βͺ ([,] β πΊ) β βͺ ([,]
β π΄)) |
86 | 81, 85 | eqssd 3966 |
1
β’ (π β βͺ ([,] β π΄) = βͺ ([,]
β πΊ)) |